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