(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/lt_arith".
-
include "nat/div_and_mod.ma".
(* plus *)
]
qed.
+lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
+intros.
+elim (le_to_or_lt_eq O ? (le_O_n m))
+ [assumption
+ |apply False_ind.
+ rewrite < H1 in H.
+ rewrite < times_n_O in H.
+ apply (not_le_Sn_O ? H)
+ ]
+qed.
+
(* times *)
theorem monotonic_lt_times_r:
\forall n:nat.monotonic nat lt (\lambda m.(S n)*m).