proposition: Lemma add_mod (a b n : nat) : (a + b) mod n = (a mod n + b mod n) mod n.
proof: Proof. apply: Nat2Z.inj. do ? rewrite !(Nat2Z.inj_mod, Nat2Z.inj_add). apply: Zplus_mod. Qed.
imports: Arith Lia ZArith.Znat ZArith.Zdiv ssreflect ssrbool ssrfun