proposition: Theorem mul_mod: forall a b n, 0<=a -> 0<=b -> 0<n -> (a * b) mod n == ((a mod n) * (b mod n)) mod n.
proof: Proof. intros a b n ? ? ?. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial. - reflexivity. - now destruct (mod_bound_pos b n). Qed.
imports: NZAxioms NZMulOrder