proposition: Lemma mod_mul_r : forall a b c, b~=0 -> c~=0 -> a rem (b*c) == a rem b + b*((a÷b) rem c).
proof: Proof. intros a b c Hb Hc. apply add_cancel_l with (b*c*(a÷(b*c))). rewrite <- quot_rem by (apply neq_mul_0; split; order). rewrite <- quot_quot by trivial. rewrite add_assoc, add_shuffle0, <- mul_assoc, <- mul_add_distr_l. rewrite <- quot_rem by order. apply quot_rem; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv