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