proposition: Lemma Z_div_plus_full : forall a b c:Z, c <> 0 -> (a + b * c) / c = a / c + b.
proof: Proof. Proof Z.div_add. Theorem Z_div_plus_full_l: forall a b c : Z, b <> 0 -> (a * b + c) / b = a + c / b. Proof Z.div_add_l. Lemma Zdiv_opp_opp : forall a b:Z, (-a)/(-b) = a/b. Proof. intros a b. zero_or_not b. apply Z.div_opp_opp; auto. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms