proposition: Lemma divide_div_mul_exact : forall a b c, b~=0 -> (b|a) -> (c*a)/b == c*(a/b).
proof: Proof. intros a b c Hb H. apply mul_cancel_l with b; trivial. rewrite mul_assoc, mul_shuffle0. assert (H':=H). apply mod_divide, div_exact in H'; trivial. rewrite <- H', (mul_comm a c). symmetry. apply div_exact; trivial. apply mod_divide; trivial. now apply divide_mul_r. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor