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