X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fle_arith.ma;h=f391c85a9686e77900e11bee558cd07987e3fbf8;hb=10f29fdd78ee089a9a94446207b543d33d6c851c;hp=6ad389346a8b9e2347493f1b0b3299866feb7869;hpb=5f6a2cf7134fda213ffc721ee7eebf5be30d7800;p=helm.git

diff --git a/helm/software/matita/library/nat/le_arith.ma b/helm/software/matita/library/nat/le_arith.ma
index 6ad389346..f391c85a9 100644
--- a/helm/software/matita/library/nat/le_arith.ma
+++ b/helm/software/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.