proposition: Lemma flip_lt_negate x y : -y < -x ↔ x < y.
proof: Proof. assert (∀ a b, a < b → -b < -a). intros a b E. setoid_replace (-b) with (-a + -b + a) by ring. setoid_replace (-a) with (-a + -b + b) at 2 by ring. now apply (strictly_order_preserving _). split; intros; auto. rewrite <-(negate_involutive x), <-(negate_involutive y); auto. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.orders.semirings