proposition: Lemma flip_le_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 (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