proposition: Lemma mod_add : forall a b c, 0<=a -> 0<=a+b*c -> 0<c -> (a + b * c) mod c == a mod c.
proof: Proof. intros a b c ? ? ?. symmetry. apply mod_unique with (a/c+b); auto. - apply mod_bound_pos; auto. - rewrite mul_add_distr_l, add_shuffle0, <- div_mod by order. now rewrite mul_comm. Qed.
imports: NZAxioms NZMulOrder