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=607a9135ef31308662bb9003febd8d85bd51a5e5;hp=e3da0c92262e6682a676a87f120711c8be8169db;hb=ccf5878f2a2ec7f952f140e162391708a740517b;hpb=5e72e41f4f86814e56d4b00959ccc56c71042a4c

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 e3da0c922..607a9135e 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma
@@ -25,6 +25,9 @@ lemma nle_minus_sn_refl_sn (m) (n): m - n ≤ m.
 #n #IH /2 width=3 by nle_trans/
 qed.
 
+lemma nle_minus_succ_sn (m) (n): ↑n - m ≤ ↑(n - m).
+// qed.
+
 (*** inv_eq_minus_O *)
 lemma nle_eq_minus_O (m) (n): 𝟎 = m - n → m ≤ n.
 #m #n @(nat_ind_2 … m n) //