x y : -y < -x <-> x < y. Proof. assert (forall a b, a < b -> -b < -a). - intros a b E. rewrite (plus_conjugate (-b) (-a)), involutive. apply lt_eq_trans with (-a + -b + b). + apply (strictly_order_preserving _). trivial. + rewrite <-plus_assoc,plus_negate_l, plus_0_r. reflexivity. - split; intros; auto. rewrite <-(negate_involutive x), <-(negate_involutive y); auto. Qed.
Require Import