proposition: Lemma char_minus_right x y : x < - y -> y < - x.
proof: Proof. intros ltnxy. rewrite <- (negate_involutive y). apply (snd (flip_lt_negate _ _)). assumption. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.interfaces.rationals HoTT.Classes.interfaces.archimedean HoTT.Classes.theory.fields HoTT.Classes.orders.rings