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

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

diff --git a/helm/matita/library/Z/compare.ma b/helm/matita/library/Z/compare.ma
index d2e075d26cb159377bed4dafd00b9912ac71891d..551bfcf8a4333854e8af5ef99a7acca21ab2ae1e 100644 (file)
--- a/helm/matita/library/Z/compare.ma
+++ b/helm/matita/library/Z/compare.ma
@@ -106,16 +106,14 @@ simplify.exact I.
 simplify.exact I.
 elim y. simplify.exact I.
 simplify. 
-(*CSC: qui uso le perche' altrimenti ci sono troppe scelte
-  per via delle coercions! *)
 cut match (nat_compare n1 n) with
 [ LT \Rightarrow n1<n
 | EQ \Rightarrow n1=n
 | GT \Rightarrow n<n1] \to 
 match (nat_compare n1 n) with
-[ LT \Rightarrow (le (S n1) n)
+[ LT \Rightarrow (S n1) \leq n
 | EQ \Rightarrow neg n = neg n1
-| GT \Rightarrow (le (S n) n1)]. 
+| GT \Rightarrow (S n) \leq n1]. 
 apply Hcut. apply nat_compare_to_Prop. 
 elim (nat_compare n1 n).
 simplify.exact H.
@@ -125,16 +123,14 @@ simplify.exact I.
 elim y.simplify.exact I.
 simplify.exact I.
 simplify.
-(*CSC: qui uso le perche' altrimenti ci sono troppe scelte
-  per via delle coercions! *)
 cut match (nat_compare n n1) with
 [ LT \Rightarrow n<n1
 | EQ \Rightarrow n=n1
 | GT \Rightarrow n1<n] \to 
 match (nat_compare n n1) with
-[ LT \Rightarrow (le (S n) n1)
+[ LT \Rightarrow (S n) \leq n1
 | EQ \Rightarrow pos n = pos n1
-| GT \Rightarrow (le (S n1) n)]. 
+| GT \Rightarrow (S n1) \leq n]. 
 apply Hcut. apply nat_compare_to_Prop. 
 elim (nat_compare n n1).
 simplify.exact H.