proposition: Lemma flip_lt_negate x y : -y < -x <-> x < y.
proof: 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.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.groups HoTT.Classes.theory.rings HoTT.Classes.orders.semirings