update in ground_2 static_2 basic_2

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / lib / arith.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index a29899d451a6b8b10152012ced8c0b7ed252839b..0574e1757927e90a2f848b7ec4e6d550891fb823 100644 (file)
--- 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)