proposition: Lemma add_mul_mod_distr_r: forall a b c d, 0<=a -> 0<b -> 0<=d<c -> (a*c+d) mod (b*c) == (a mod b)*c+d.
proof: Proof. intros a b c d ? ? ?. now rewrite !(mul_comm _ c), add_mul_mod_distr_l. Qed.
imports: NZAxioms NZMulOrder