proposition: Theorem Zdiv_neg a b: a < 0 -> 0 < b -> a / b < 0.
proof: Proof. intros Ha Hb. assert (b > 0) by lia. generalize (Z_mult_div_ge a _ H); intros. assert (b * (a / b) < 0)%Z. apply Z.le_lt_trans with a; auto with zarith. destruct b; try (compute in Hb; discriminate). destruct (a/Zpos p)%Z. compute in H1; discriminate. compute in H1; discriminate. compute; auto. Qed.
imports: ArithRing ZArith Znumtheory Zpow_facts Lia