proposition: Lemma divide_quot_mul_exact : forall a b c, b~=0 -> (b|a) -> (c*a)÷b == c*(a÷b).
proof: Proof. intros a b c Hb H. rewrite 2 quot_div_exact; trivial. - apply divide_div_mul_exact; trivial. - now apply divide_mul_r. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor