(x y z : R) : z < y - x <-> z + x < y. 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.
Require Import