(* *)
(**************************************************************************)
-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).
]
qed.
-theorem le_times_to_le_div: \forall a,b,c:nat.
-O \lt b \to (b*c) \le a \to c \le (a /b).
-intros.
-apply lt_S_to_le.
-apply (lt_times_n_to_lt b)
- [assumption
- |rewrite > sym_times.
- apply (le_to_lt_to_lt ? a)
- [assumption
- |simplify.
- rewrite > sym_plus.
- rewrite > (div_mod a b) in ⊢ (? % ?)
- [apply lt_plus_r.
- apply lt_mod_m_m.
- assumption
- |assumption
- ]
- ]
- ]
-qed.
+
theorem nat_compare_times_l : \forall n,p,q:nat.
nat_compare p q = nat_compare ((S n) * p) ((S n) * q).