proposition: Lemma mul_mod_idemp_l : forall a b n, n~=0 -> ((a mod n)*b) mod n == (a*b) mod n.
proof: Proof. intros a b n Hn. symmetry. rewrite (div_mod a n) at 1 by order. rewrite add_comm, (mul_comm n), (mul_comm _ b). rewrite mul_add_distr_l, mul_assoc. rewrite mod_add by trivial. now rewrite mul_comm. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv