X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fnat.ma;h=8613043b8d70c0705af03428371be11ea63b3a1d;hb=bec531b57a008238f67cd72edc751844d28b374f;hp=bd23c6dd745b49aba23536916462306e4cf265df;hpb=3a9f692052e85ac6f00c9bfc83e4c672dc81fd6c;p=helm.git

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index bd23c6dd7..8613043b8 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -475,6 +475,11 @@ lemma le_or_ge: ∀m,n. m ≤ n ∨ n ≤ m.
 #m #n elim (decidable_le m n) /2/ /4/
 qed-.
 
+lemma le_inv_S1: ∀x,y. S x ≤ y → ∃∃z. x ≤ z & y = S z.
+#x #y #H elim H -y /2 width=3 by ex2_intro/
+#y #_ * #n #Hxn #H destruct /3 width=3 by le_S, ex2_intro/
+qed-. 
+
 (* More general conclusion **************************************************)
 
 theorem nat_ind_plus: ∀R:predicate nat.