X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_le.ma;h=ae98e3a5e52a1bba77325c67983178e5cbd83185;hp=73c14396423e316aea768fe307e290c4108abb85;hb=68e028d053806177e218ee1a5f8778d3011bef83;hpb=ccf5878f2a2ec7f952f140e162391708a740517b

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma
index 73c143964..ae98e3a5e 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma
@@ -45,7 +45,7 @@ lemma nle_succ_bi (m) (n): m ≤ n → ↑m ≤ ↑n.
 qed.
 
 (*** le_or_ge *)
-lemma nle_ge_e (m) (n): ∨∨ m ≤ n | n ≤ m.
+lemma nle_ge_dis (m) (n): ∨∨ m ≤ n | n ≤ m.
 #m @(nat_ind … m) -m [ /2 width=1 by or_introl/ ]
 #m #IH #n @(nat_ind … n) -n [ /2 width=1 by or_intror/ ]
 #n #_ elim (IH n) -IH /3 width=2 by nle_succ_bi, or_introl, or_intror/
@@ -117,7 +117,7 @@ qed-.
 
 (*** decidable_le *)
 lemma nle_dec (m) (n): Decidable … (m ≤ n).
-#m #n elim (nle_ge_e m n) [ /2 width=1 by or_introl/ ]
+#m #n elim (nle_ge_dis m n) [ /2 width=1 by or_introl/ ]
 #Hnm elim (eq_nat_dec m n) [ #H destruct /2 width=1 by nle_refl, or_introl/ ]
 /4 width=1 by nle_antisym, or_intror/
 qed-.