proposition: Theorem Z_div_mul_swap : ∀ a b c, (b | a)%Z → (a / b * c = a * c / b)%Z.
proof: Proof. intros a b c H. destruct H as (d, H). subst a. destruct (Z_zerop b) as [Hb| Hb]. subst b; rewrite Z.mul_0_r. reflexivity. rewrite Z.div_mul; [ idtac | assumption ]. rewrite Z.mul_shuffle0. rewrite Z.div_mul; [ idtac | assumption ]. reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted Psatz