proposition: Lemma mul_mod_idemp_l : forall a b n, 0<=a -> 0<=b -> 0<n -> ((a mod n)*b) mod n == (a*b) mod n.
proof: Proof. intros a b n Ha Hb Hn. symmetry. generalize (mul_nonneg_nonneg _ _ Ha Hb). rewrite (div_mod a n) at 1 2 by order. rewrite add_comm, (mul_comm n), (mul_comm _ b). rewrite mul_add_distr_l, mul_assoc. intros. rewrite mod_add; auto. - now rewrite mul_comm. - apply mul_nonneg_nonneg; destruct (mod_bound_pos a n); auto. Qed.
imports: NZAxioms NZMulOrder