proposition: Lemma flip_pos_negate x : 0 < x ↔ -x < 0.
proof: Proof. split; intros E. rewrite <- negate_0. now apply flip_lt_negate. apply flip_lt_negate. now rewrite negate_0. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.orders.semirings