proposition: Lemma flip_le_minus_r (x y z : R) : z ≤ y - x <-> z + x ≤ y.
proof: Proof. split; intros E. - rewrite plus_comm. rewrite (plus_conjugate_alt y x). apply (order_preserving _). trivial. - rewrite plus_comm. rewrite (plus_conjugate_alt z (- x)), involutive. apply (order_preserving _). trivial. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.groups HoTT.Classes.theory.rings HoTT.Classes.orders.semirings