+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.
+