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

diff --git a/helm/software/matita/library/nat/le_arith.ma b/helm/software/matita/library/nat/le_arith.ma
index 90f3e182b..9ab53fd74 100644
--- a/helm/software/matita/library/nat/le_arith.ma
+++ b/helm/software/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.