proposition: Lemma add_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_assoc, add_comm, mul_comm. intros. now rewrite mod_add. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv