Towards chebyshev.

[helm.git] / matita / library / nat / le_arith.ma

diff --git a/matita/library/nat/le_arith.ma b/matita/library/nat/le_arith.ma
index 6ad389346a8b9e2347493f1b0b3299866feb7869..f391c85a9686e77900e11bee558cd07987e3fbf8 100644 (file)
--- a/matita/library/nat/le_arith.ma
+++ b/matita/library/nat/le_arith.ma
@@ -146,6 +146,18 @@ apply nat_elim2;intros
   ]
 qed.
 
+theorem le_S_times_SSO: \forall n,m.O < m \to
+n \le m \to S n \le (S(S O))*m.
+intros.
+simplify.
+rewrite > plus_n_O.
+simplify.rewrite > plus_n_Sm.
+apply le_plus
+  [assumption
+  |rewrite < plus_n_O.
+   assumption
+  ]
+qed.
 (*0 and times *)
 theorem O_lt_const_to_le_times_const:  \forall a,c:nat.
 O \lt c \to a \le a*c.