- libraryObjects: new default "natural numbers" with the uri of nat.

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

diff --git a/helm/software/matita/library/nat/le_arith.ma b/helm/software/matita/library/nat/le_arith.ma
index 6ad389346a8b9e2347493f1b0b3299866feb7869..a222d36bab2df5b26df3782439656478c936caae 100644 (file)
--- 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.