proposition: Lemma Zplus_mod_idemp_l: forall a b n, (a mod n + b) mod n = (a + b) mod n.
proof: Proof. intros; rewrite Zplus_mod, Zmod_mod, <- Zplus_mod; auto. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms