X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fle_arith.ma;h=a222d36bab2df5b26df3782439656478c936caae;hb=dc74ed7c4af1aa9b90fc5d2f0a86bd7825696e71;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..a222d36ba 100644
--- a/helm/software/matita/library/nat/le_arith.ma
+++ b/helm/software/matita/library/nat/le_arith.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/le_arith".
-
 include "nat/times.ma".
 include "nat/orders.ma".
 
@@ -146,6 +144,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.