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