proposition: Lemma sub_mod_0: forall (a b m: Z), a mod m = 0 -> b mod m = 0 -> (a - b) mod m = 0.
proof: Proof. intros *. intros E1 E2. rewrite Zminus_mod. rewrite E1. rewrite E2. reflexivity. Qed.
imports: Coq.Classes.Morphisms Coq.ZArith.BinInt Coq.micromega.Lia Coq.ZArith.ZArith