+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 "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
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)).
qed.
(*
-theorem pippo: \forall m,n. (le (S m) (S n)) \to (le m n).
-intros.
-lapply le_gen_S_x.
+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.
*)