-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