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
theorem le_gen_S_S_cc: \forall m,n. (le m n) \to (le (S m) (S n)).
intros. auto.
qed.
+
(*
theorem le_trans: \forall x,y. (le x y) \to \forall z. (le y z) \to (le x z).
-intros 1.
-elim x. auto.
-fwd H1 [].
+intros 1. elim x; clear H. clear x.
+auto.
+fwd H1 [H]. decompose H.
*)