proposition: Theorem add_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 add_mod_idemp_l, add_mod_idemp_r; trivial. - reflexivity. - now destruct (mod_bound_pos b n). Qed.
imports: NZAxioms NZMulOrder