(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/div_and_mod_diseq".
-
include "nat/lt_arith.ma".
(* the proof that
assumption.
qed.
-theorem lt_times_to_lt_div: \forall m,n,q. O < q \to
-n < m*q \to n/q < m.
+theorem lt_times_to_lt_div: \forall m,n,q. n < m*q \to n/q < m.
intros.
-apply (lt_times_to_lt q ? ? H).
+apply (lt_times_to_lt q ? ? (lt_times_to_lt_O ? ? ? H)).
rewrite > sym_times.
rewrite > sym_times in ⊢ (? ? %).
apply (le_plus_to_le (n \mod q)).
[assumption
|apply le_plus_n
]
- |assumption
+ |apply (lt_times_to_lt_O ? ? ? H)
]
qed.
theorem lt_div: \forall n,m. O < m \to S O < n \to m/n < m.
intros.
-apply lt_times_to_lt_div
- [apply lt_to_le. assumption
- |rewrite > sym_times.
- apply lt_m_nm;assumption
- ]
+apply lt_times_to_lt_div.
+rewrite < sym_times.
+apply lt_m_nm;assumption.
qed.
theorem le_div_plus_S: \forall m,n,q. O < q \to
(m+n)/q \le S(m/q + n/q).
intros.
apply le_S_S_to_le.
-apply lt_times_to_lt_div
- [assumption
- |change in ⊢ (? ? %) with (q + (q + (m/q+n/q)*q)).
- rewrite > sym_times.
- rewrite > distr_times_plus.
- rewrite > sym_times.
- rewrite < assoc_plus in ⊢ (? ? (? ? %)).
- rewrite < assoc_plus.
- rewrite > sym_plus in ⊢ (? ? (? % ?)).
- rewrite > assoc_plus.
- apply lt_plus
- [change with (m < S(m/q)*q).
- apply lt_div_S.
- assumption
- |rewrite > sym_times.
- change with (n < S(n/q)*q).
- apply lt_div_S.
- assumption
- ]
+apply lt_times_to_lt_div.
+change in ⊢ (? ? %) with (q + (q + (m/q+n/q)*q)).
+rewrite > sym_times.
+rewrite > distr_times_plus.
+rewrite > sym_times.
+rewrite < assoc_plus in ⊢ (? ? (? ? %)).
+rewrite < assoc_plus.
+rewrite > sym_plus in ⊢ (? ? (? % ?)).
+rewrite > assoc_plus.
+apply lt_plus
+ [change with (m < S(m/q)*q).
+ apply lt_div_S.
+ assumption
+ |rewrite > sym_times.
+ change with (n < S(n/q)*q).
+ apply lt_div_S.
+ assumption
]
qed.