X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Farith.ma;h=0574e1757927e90a2f848b7ec4e6d550891fb823;hb=a67fc50ccfda64377e2c94c18c3a0d9265f651db;hp=a29899d451a6b8b10152012ced8c0b7ed252839b;hpb=fb4c641d43be3d601104751363782553bea0fb6b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index a29899d45..0574e1757 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -127,6 +127,14 @@ qed-.
 lemma le_plus_to_minus_comm: ∀n,m,p. n ≤ p+m → n-p ≤ m.
 /2 width=1 by le_plus_to_minus/ qed-.
 
+lemma le_inv_S1: ∀m,n. ↑m ≤ n → ∃∃p. m ≤ p & ↑p = n.
+#m *
+[ #H lapply (le_n_O_to_eq … H) -H
+  #H destruct
+| /3 width=3 by monotonic_pred, ex2_intro/
+]
+qed-.
+
 (* Note: this might interfere with nat.ma *)
 lemma monotonic_lt_pred: ∀m,n. m < n → 0 < m → pred m < pred n.
 #m #n #Hmn #Hm whd >(S_pred … Hm)