some theorems have been moved to more appropriate files in library.

[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 90f3e182b2f51441b34c06054816a6c1cdcc9a82..9ab53fd7405a1946cf555974992c922dbdcc2acb 100644 (file)
--- 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.