proposition: Theorem Zminus_mod: forall a b n, (a - b) mod n = (a mod n - b mod n) mod n.
proof: Proof. intros a b n. replace (a - b) with (a + (-1) * b); auto with zarith. replace (a mod n - b mod n) with (a mod n + (-1) * (b mod n)); auto with zarith. rewrite Zplus_mod. rewrite Zmult_mod. rewrite (Zplus_mod _ ((-1) * (b mod n))). rewrite Zmult_mod. rewrite (Zmult_mod _ (b mod n)). repeat rewrite Zmod_mod; auto. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms