(* *)
(**************************************************************************)
-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.
]
qed.
+theorem le_div_times_Sm: \forall a,i,m. O < i \to O < m \to
+a / i \le (a * S (m / i))/m.
+intros.
+apply (trans_le ? ((a * S (m / i))/((S (m/i))*i)))
+ [rewrite < (eq_div_div_div_times ? i)
+ [rewrite > lt_O_to_div_times
+ [apply le_n
+ |apply lt_O_S
+ ]
+ |apply lt_O_S
+ |assumption
+ ]
+ |apply le_times_to_le_div
+ [assumption
+ |apply (trans_le ? (m*(a*S (m/i))/(S (m/i)*i)))
+ [apply le_times_div_div_times.
+ rewrite > (times_n_O O).
+ apply lt_times
+ [apply lt_O_S
+ |assumption
+ ]
+ |rewrite > sym_times.
+ apply le_times_to_le_div2
+ [rewrite > (times_n_O O).
+ apply lt_times
+ [apply lt_O_S
+ |assumption
+ ]
+ |apply le_times_r.
+ apply lt_to_le.
+ apply lt_div_S.
+ assumption
+ ]
+ ]
+ ]
+ ]
+qed.
+