proposition: Lemma flip_neg_minus (x y : R) : y - x < 0 ↔ y < x.
proof: Proof. setoid_replace x with (0 + x) at 2 by ring. now apply flip_lt_minus_l. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.orders.semirings