proposition: Lemma mod_add_r: forall a b, b <> 0 -> (a + b) mod b = a mod b.
proof: Proof. intros. rewrite <- Z.add_mod_idemp_r by lia. rewrite Z.mod_same by lia. rewrite Z.add_0_r. reflexivity. Qed.
imports: Coq.Classes.Morphisms Coq.ZArith.BinInt Coq.micromega.Lia Coq.ZArith.ZArith