X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_le.ma;h=a2bffd82c47fe054c4d83563a339e1bb90215661;hb=d7a1ab434c222c2445f36b7a3b6234d1f57f9794;hp=c2d89a6f76f5e273b2bc1eba015daaa2b12df051;hpb=ca318d6d92098c3a65c9f0841174ca110c82e064;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma
index c2d89a6f7..a2bffd82c 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma
@@ -18,9 +18,10 @@ include "ground/arith/nat_succ.ma".
 (* ORDER FOR NON-NEGATIVE INTEGERS ******************************************)
 
 (*** le *)
-(*** le_ind *)
 inductive nle (m:nat): predicate nat ≝
+(*** le_n *)
 | nle_refl   : nle m m
+(*** le_S *)
 | nle_succ_dx: ∀n. nle m n → nle m (↑n)
 .
 
@@ -88,7 +89,7 @@ lemma nle_inv_succ_zero (m): ↑m ≤ 𝟎 → ⊥.
 
 lemma nle_inv_succ_sn_refl (m): ↑m ≤ m → ⊥.
 #m @(nat_ind_succ … m) -m [| #m #IH ] #H
-[ /3 width=2 by nle_inv_zero_dx, eq_inv_zero_nsucc/
+[ /2 width=2 by nle_inv_succ_zero/
 | /3 width=1 by nle_inv_succ_bi/
 ]
 qed-.
@@ -110,7 +111,7 @@ lemma nle_ind_alt (Q: relation2 nat nat):
       (∀m,n. m ≤ n → Q m n → Q (↑m) (↑n)) →
       ∀m,n. m ≤ n → Q m n.
 #Q #IH1 #IH2 #m #n @(nat_ind_2_succ … m n) -m -n //
-[ #m #H elim (nle_inv_succ_zero … H)
+[ #m #_ #H elim (nle_inv_succ_zero … H)
 | /4 width=1 by nle_inv_succ_bi/
 ]
 qed-.