X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Farithmetics%2Fnat.ma;h=31d5ced7f7c64ac7dfa03ee8b6f96c65ad12a09b;hb=84713c9446ff13dd26533590985a0df67cb5ec7e;hp=44c3119fae1fad9be401452f9c4a667eb813a050;hpb=ae6757199708cc32166961debb52d48114c0eb74;p=helm.git

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 44c3119fa..31d5ced7f 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -374,6 +374,9 @@ theorem lt_plus_to_minus_r: ∀a,b,c. a + b < c → a < c - b.
 #a #b #c #H @le_plus_to_minus_r //
 qed.
 
+lemma lt_plus_Sn_r: ∀a,x,n. a < a + x + (S n).
+/2 width=1/ qed.
+
 theorem lt_S_S_to_lt: ∀n,m:nat. S n < S m → n < m.
 (* demo *)
 /2/ qed-.
@@ -780,4 +783,3 @@ lemma le_maxr: ∀i,n,m. max n m ≤ i → m ≤ i.
 lemma to_max: ∀i,n,m. n ≤ i → m ≤ i → max n m ≤ i.
 #i #n #m #leni #lemi normalize (cases (leb n m)) 
 normalize // qed.
-