proposition: Theorem Z_quot_plus_l: forall a b c : Z, 0 <= (a*b+c)*c -> b<>0 -> b<>0 -> (a * b + c) ÷ b = a + c ÷ b.
proof: Proof. intros. apply Z.quot_add_l; auto with zarith. Qed.
imports: Nnat ZArith_base Lia ZArithRing Zdiv Morphisms