-set "baseuri" "cic:/matita/tests/".
+set "baseuri" "cic:/matita/tests/fguidi/".
alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
alias id "False_ind" = "cic:/Coq/Init/Logic/False_ind.con".
alias id "I" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1/1)".
alias id "ex_intro" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1/1)".
+alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
+alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
alias symbol "and" (instance 0) = "logical and".
alias symbol "eq" (instance 0) = "leibnitz's equality".
alias symbol "exists" (instance 0) = "exists".
-alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
-alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
definition is_S: nat \to Prop \def
\lambda n. match n with
theorem le_gen_x_O_aux: \forall x, y. (le x y) \to (y =O) \to
(x = O).
-intros 3. elim H. auto. apply eq_gen_S_O. exact x2. auto.
+intros 3. elim H. auto. apply eq_gen_S_O. exact n1. auto.
qed.
theorem le_gen_x_O: \forall x. (le x O) \to (x = O).
(\exists n. x = (S n) \land (le m n)).
intros 4. elim H.
apply eq_gen_S_O. exact m. elim H1. auto.
-cut x1 = m. elim Hcut. apply ex_intro. exact x2. auto. auto.
+cut n = m. elim Hcut. apply ex_intro. exact n1. auto. auto.
qed.
theorem le_gen_S_x: \forall m,x. (le (S m) x) \to
qed.
theorem le_gen_S_S: \forall m,n. (le (S m) (S n)) \to (le m n).
-intros. cut (\exists p. (S n) = (S p) \land (le m p)).
-elim Hcut. elim H1. cut x = n.
-elim Hcut1. auto. symmetry. auto. auto.
+intros.
+lapply le_gen_S_x to H using H0. elim H0. elim H1.
+lapply eq_gen_S_S to H2 using H4. rewrite > H4. assumption.
qed.
theorem le_gen_S_S_cc: \forall m,n. (le m n) \to (le (S m) (S n)).
intros. auto.
qed.
-theorem le_gen_S_x_2: \forall m,x. (le (S m) x) \to
- \exists n. x = (S n) \land (le m n).
-intros.
-lapply le_gen_S_x to H using H0. elim H0. elim H1.
-exists. exact x1. auto.
-qed.
-
-(* proof of le_gen_S_S with lapply *)
-theorem le_gen_S_S_2: \forall m,n. (le (S m) (S n)) \to (le m n).
-intros.
-lapply le_gen_S_x_2 to H using H0. elim H0. elim H1.
-lapply eq_gen_S_S to H2 using H4. rewrite left H4. assumption.
-qed.
+(*
+theorem le_trans: \forall x,y. (le x y) \to \forall z. (le y z) \to (le x z).
+intros 1. elim x; clear H. clear x.
+auto.
+fwd H1 [H]. decompose H.
+*)