proposition: Lemma mul_rem_distr_r: forall a b c, b~=0 -> c~=0 -> (a*c) rem (b*c) == (a rem b) * c.
proof: Proof. intros a b c **. assert (b*c ~= 0) by (rewrite <- neq_mul_0; tauto). rewrite ! rem_eq by trivial. rewrite quot_mul_cancel_r by order. now rewrite mul_sub_distr_r, <- !mul_assoc, (mul_comm (a÷b) c). Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv