proposition: Theorem mul_le_mono_neg_l : forall n m p, p < 0 -> (n <= m <-> p * m <= p * n).
proof: Proof. intros n m p H; do 2 rewrite lt_eq_cases. rewrite (mul_lt_mono_neg_l p n m); [| assumption]. rewrite -> (mul_cancel_l m n p) by (intro H1; rewrite H1 in H; false_hyp H lt_irrefl). now setoid_replace (n == m) with (m == n) by (split; now intro). Qed.
imports: NZAxioms NZAddOrder