proposition: Lemma mul_mod_distr_l: forall a b c, 0<=a -> 0<b -> 0<c -> (c*a) mod (c*b) == c * (a mod b).
proof: Proof. intros a b c ? ? ?. pose proof (E := add_mul_mod_distr_l a b c 0). rewrite ? add_0_r in E. now apply E. Qed.
imports: NZAxioms NZMulOrder