proposition: Lemma add_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 (add_nonneg_nonneg _ _ Ha Hb). rewrite (div_mod a n) at 1 2 by order. rewrite <- add_assoc, add_comm, mul_comm. intros. rewrite mod_add; trivial. - reflexivity. - apply add_nonneg_nonneg; auto. destruct (mod_bound_pos a n); auto. Qed.
imports: NZAxioms NZMulOrder