proposition: Lemma mul_mod_distr_l: forall a b c, b~=0 -> c~=0 -> (c*a) mod (c*b) == c * (a mod b).
proof: Proof. intros a b c **. rewrite <- (add_cancel_l _ _ ((c*b)* ((c*a)/(c*b)))). rewrite <- div_mod. - rewrite div_mul_cancel_l by trivial. rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order. apply div_mod; order. - rewrite <- neq_mul_0; auto. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv