proposition: Lemma Z_div_neg : forall a b : Z, (0 < b)%Z -> (a < 0)%Z -> (a / b < 0)%Z.
proof: Proof. intros. rewrite (Z_div_mod_eq_full a b) in H0. elim (Z_mod_lt a b). intros H1 _. apply Znot_ge_lt. intro. apply (Zlt_not_le (b * (a / b) + a mod b) 0 H0). apply Zplus_le_0_compat. apply Zmult_le_0_compat. apply Zlt_le_weak; assumption. Flip. assumption. Flip. Qed.
imports: Coq(Lia)