X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Fle_arith.ma;h=9ab53fd7405a1946cf555974992c922dbdcc2acb;hb=b49683e0bc65391911be8b1e648ddb1ec61665b9;hp=90f3e182b2f51441b34c06054816a6c1cdcc9a82;hpb=314d68672678df5b00359145150395fcba8b4e8c;p=helm.git

diff --git a/matita/library/nat/le_arith.ma b/matita/library/nat/le_arith.ma
index 90f3e182b..9ab53fd74 100644
--- a/matita/library/nat/le_arith.ma
+++ b/matita/library/nat/le_arith.ma
@@ -131,4 +131,15 @@ apply nat_elim2;intros
      assumption
     ]
   ]
-qed.
\ No newline at end of file
+qed.
+
+(*0 and times *)
+theorem O_lt_const_to_le_times_const:  \forall a,c:nat.
+O \lt c \to a \le a*c.
+intros.
+rewrite > (times_n_SO a) in \vdash (? % ?).
+apply le_times
+[ apply le_n
+| assumption
+]
+qed.