proposition: Lemma flip_neg_negate x : x < 0 ↔ 0 < -x.
proof: Proof. rewrite <-(negate_involutive x) at 1. split; intros; now apply flip_pos_negate. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.orders.semirings