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