proposition: Lemma flip_le_minus_r (x y z : R) : z ≤ y - x ↔ z + x ≤ y.
proof: Proof. split; intros E. rewrite commutativity. setoid_replace y with (x + (y - x)) by ring. now apply (order_preserving _). rewrite commutativity. setoid_replace z with (-x + (z + x)) by ring. now apply (order_preserving _). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.orders.semirings