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