-theorem le_div: \forall n,m. O < n \to m/n \le m.
-intros.
-rewrite > (div_mod m n) in \vdash (? ? %)
- [apply (trans_le ? (m/n*n))
- [rewrite > times_n_SO in \vdash (? % ?).
- apply le_times
- [apply le_n|assumption]
- |apply le_plus_n_r
- ]
- |assumption
- ]
-qed.
-