removed work-arounds for poor disambiguation, which should now be fixed with the...

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

diff --git a/helm/matita/library/Z/orders.ma b/helm/matita/library/Z/orders.ma
index bc5ffdb5125f5495b3df6ee878c2cef0e7f04488..ec1d6fb525f8a270f6058ebfba7f13118ee44fc9 100644 (file)
--- a/helm/matita/library/Z/orders.ma
+++ b/helm/matita/library/Z/orders.ma
@@ -73,26 +73,22 @@ qed.
 theorem irrefl_Zlt: irreflexive Z Zlt
 \def irreflexive_Zlt.
 
-(*CSC: qui uso lt perche' ho due istanze diverse di < *)
 theorem Zlt_neg_neg_to_lt: 
-\forall n,m:nat. neg n < neg m \to lt m n.
+\forall n,m:nat. neg n < neg m \to m < n.
 intros.apply H.
 qed.
 
-(*CSC: qui uso lt perche' ho due istanze diverse di < *)
-theorem lt_to_Zlt_neg_neg: \forall n,m:nat.lt m n \to neg n < neg m. 
+theorem lt_to_Zlt_neg_neg: \forall n,m:nat.m < n \to neg n < neg m. 
 intros.
 simplify.apply H.
 qed.
 
-(*CSC: qui uso lt perche' ho due istanze diverse di < *)
 theorem Zlt_pos_pos_to_lt: 
-\forall n,m:nat. pos n < pos m \to lt n m.
+\forall n,m:nat. pos n < pos m \to n < m.
 intros.apply H.
 qed.
 
-(*CSC: qui uso lt perche' ho due istanze diverse di < *)
-theorem lt_to_Zlt_pos_pos: \forall n,m:nat.lt n m \to pos n < pos m. 
+theorem lt_to_Zlt_pos_pos: \forall n,m:nat.n < m \to pos n < pos m. 
 intros.
 simplify.apply H.
 qed.