proposition: Lemma Zplus_rem_idemp_l: forall a b n, 0 <= a * b -> Z.rem (Z.rem a n + b) n = Z.rem (a + b) n.
proof: Proof. intros. zero_or_not n. apply Z.add_rem_idemp_l; auto. Qed.
imports: Nnat ZArith_base Lia ZArithRing Zdiv Morphisms