qed.
(* ??? this needs not le *)
-theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
+theorem S_pred: \forall n:nat.lt O n \to n=S (pred n).
intro.elim n.apply False_ind.exact not_le_Sn_O O H.
apply eq_f.apply pred_Sn.
qed.
qed.
(* le elimination *)
-theorem le_n_O_to_eq : \forall n:nat. (le n O) \to (eq nat O n).
+theorem le_n_O_to_eq : \forall n:nat. (le n O) \to O=n.
intro.elim n.reflexivity.
apply False_ind.
(* non si applica not_le_Sn_O *)
qed.
theorem le_n_Sm_elim : \forall n,m:nat.le n (S m) \to
-\forall P:Prop. (le (S n) (S m) \to P) \to (eq nat n (S m) \to P) \to P.
+\forall P:Prop. (le (S n) (S m) \to P) \to (n=(S m) \to P) \to P.
intros 4.elim H.
apply H2.reflexivity.
apply H3. apply le_S_S. assumption.
(* other abstract properties *)
theorem antisymmetric_le : antisymmetric nat le.
simplify.intros 2.
-apply nat_elim2 (\lambda n,m.((le n m) \to (le m n) \to eq nat n m)).
+apply nat_elim2 (\lambda n,m.((le n m) \to (le m n) \to n=m)).
intros.apply le_n_O_to_eq.assumption.
intros.apply False_ind.apply not_le_Sn_O ? H.
intros.apply eq_f.apply H.
apply le_S_S_to_le.assumption.
qed.
-theorem antisym_le: \forall n,m:nat. le n m \to le m n \to eq nat n m
+theorem antisym_le: \forall n,m:nat. le n m \to le m n \to n=m
\def antisymmetric_le.
theorem decidable_le: \forall n,m:nat. decidable (le n m).
intros 2.simplify.intro.elim H.
left.apply le_S_S.assumption.
right.intro.apply H1.apply le_S_S_to_le.assumption.
-qed.
\ No newline at end of file
+qed.