proposition: Lemma Z_mod_plus_full : forall a b c:Z, (a + b * c) mod c = a mod c.
proof: Proof. intros a b c. zero_or_not c. - now rewrite Z.mul_0_r, Z.add_0_r. - now apply Z.mod_add. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms