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