-theorem eq_div_times_div_times: \forall a,b,c:nat.
-O \lt b \to b \divides a \to b \divides c \to
-a / b * c = a * (c/b).
-intros.
-elim H1.
-elim H2.
-rewrite > H3.
-rewrite > H4.
-rewrite > (sym_times) in \vdash (? ? ? (? ? (? % ?))).
-rewrite > (sym_times) in \vdash (? ? (? (? % ?) ?) ?).
-rewrite > (lt_O_to_div_times ? ? H).
-rewrite > (lt_O_to_div_times ? ? H) in \vdash (? ? ? (? ? %)).
-rewrite > (sym_times b n2).
-rewrite > assoc_times.
-reflexivity.
-qed.
-