proposition: Lemma mod_add : forall a b c, c~=0 -> (a + b * c) mod c == a mod c.
proof: Proof. intros. symmetry. apply mod_unique with (a/c+b); trivial. - now apply mod_always_pos. - rewrite mul_add_distr_l, add_shuffle0, <- div_mod by order. now rewrite mul_comm. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv