Notation for equality used everywhere.

[helm.git] / helm / matita / library / nat / orders.ma

diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma
index 34cd6f6a3aa2adc7eeedf033616aa5b9d5ea79c5..3f788c6506c11ebd62f638c02e2f1cd68c031783 100644 (file)
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -84,7 +84,7 @@ apply le_S_S_to_le.assumption.
 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.
@@ -112,7 +112,7 @@ apply H2.apply lt_to_le. apply H3.
 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 *)
@@ -128,7 +128,7 @@ apply  (not_le_Sn_O ? H1).
 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.
@@ -137,7 +137,7 @@ qed.
 (* 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.
@@ -145,7 +145,7 @@ apply le_S_S_to_le.assumption.
 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).
@@ -156,4 +156,4 @@ intros.simplify.right.exact not_le_Sn_O n1.
 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.