(* This proof is really in Heyting Arithmetic *)
Lemma eq_dec : forall x y:nat, x=y \/ ~x=y.
induction x.
Admitted.
(* this is just auxiliary for later *)
Lemma addnS : forall x y, x + (S y) = S (x + y).
induction x.
Admitted.
(* Here we do a proof with constructive content *)
Lemma div_constr : forall x, exists y, x = y + y \/ x = S(y + y).
(* important, once done finish your proof with "Defined." instead of "Qed." *)
Admitted.
Eval compute in (div_constr 90).
Eval compute in (div_constr 91).
Lemma moins: forall x y, exists z, x = y + z \/ y = x + z.
Admitted.
Lemma addn0 : forall x, x + 0 = x.
Admitted.
Lemma add_comm: forall x y, x + y = y + x.
Admitted.
(* not essential; playing with decidability *)
Lemma dec_and :
forall A B, (A\/~A) -> (B\/~B) -> (A/\B) \/ ~(A/\B).
Admitted.
Lemma dec_or :
forall A B, (A\/~A) -> (B\/~B) -> (A\/B) \/ ~(A\/B).
Admitted.
Lemma dec_imp :
forall A B, (A\/~A) -> (B\/~B) -> (A->B) \/ ~(A->B).
Admitted.
Parameter eps : (nat -> Prop) -> nat.
Axiom eps_a : forall (P:nat->Prop) n, P n -> P (eps P).
Lemma ex_dec : forall (P:nat->Prop),
(forall x, P x \/ ~P x) -> (exists x, P x) \/ ~exists x, (P x).
Admitted.
(* This one requires a litle more Coq syntax *)
Lemma fa_dec : forall (P:nat->Prop),
(forall x, P x \/ ~P x) -> (forall x, P x) \/ ~forall x, (P x).
Admitted.