proposition: Lemma flip_lt_minus_r (x y z : R) : z < y - x <-> z + x < y.
proof: Proof. split; intros E. - rewrite plus_comm, (plus_conjugate_alt y x). apply (strictly_order_preserving _). trivial. - rewrite plus_comm, (plus_conjugate_alt z (-x)), involutive. apply (strictly_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