proposition: Lemma flip_le_minus_l (x y z : R) : y - x ≤ z ↔ y ≤ z + x.
proof: Proof. rewrite <-(negate_involutive x) at 2. split; now apply flip_le_minus_r. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.orders.semirings