X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_le_minus.ma;h=507cdd2b60365a44df9799a88d006a2772ff758e;hp=5656acffd1c61acc1eb9a4618f91a057f12d8370;hb=19b0a814861157ba05f23877d5cd94059f52c2e8;hpb=21de0d35017656c5a55528390b54b0b2ae395b44

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma
index 5656acffd..507cdd2b6 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma
@@ -30,7 +30,7 @@ lemma nle_minus_succ_sn (m) (n): ↑n - m ≤ ↑(n - m).
 
 (*** inv_eq_minus_O *)
 lemma nle_eq_minus_O (m) (n): 𝟎 = m - n → m ≤ n.
-#m #n @(nat_ind_succ_2 … m n) //
+#m #n @(nat_ind_2_succ … m n) //
 /3 width=1 by nle_succ_bi/
 qed.
 
@@ -46,6 +46,10 @@ lemma nle_minus_dx_bi (m) (n) (o): m ≤ n → o-n ≤ o-m.
 #n #_ #IH /2 width=3 by nle_trans/
 qed.
 
+(*** minus_le_trans_sn *)
+lemma nle_minus_sn (o) (m) (n): m ≤ n → m - o ≤ n.
+/2 width=3 by nle_trans/ qed.
+
 (* Inversions with nminus ***************************************************)
 
 (*** eq_minus_O *)