x y : -y ≤ -x <-> x ≤ y. Proof. assert (forall a b, a ≤ b -> -b ≤ -a). - intros a b E. transitivity (-a + -b + a);[apply eq_le| transitivity (-a + -b + b);[|apply eq_le]]. + rewrite plus_comm, plus_assoc, plus_negate_r, plus_0_l. reflexivity. + apply (order_preserving _). trivial. + rewrite <-plus_assoc, plus_negate_l. apply plus_0_r. - split; intros; auto. rewrite <-(negate_involutive x), <-(negate_involutive y); auto. Qed.
Require Import