proposition: Lemma sub_mod_0: forall (a b m: nat), a mod m = 0 -> b mod m = 0 -> (a - b) mod m = 0.
proof: Proof. intros. assert (m = 0 \/ m <> 0) as C by lia. destruct C as [C | C]. - subst. rewrite mod_0_r in *. simpl in *. now subst. - assert (a - b = 0 \/ b < a) as D by lia. destruct D as [D | D]. + rewrite D. apply Nat.mod_0_l. assumption. + apply Nat2Z.inj. rewrite Nat2Z.inj_mod. rewrite Nat2Z.inj_sub by lia. rewrite Zdiv.Zminus_mod. rewrite <-! Nat2Z.inj_mod. rewrite H. rewrite H0. apply Z.mod_0_l. lia. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Bool.Bool Coq.Arith.Arith Coq.micromega.Lia Coq.NArith.NArith Coq.ZArith.ZArith bbv.N_Z_nat_conversions bbv.Nomega