proposition: Lemma eq_not_lt x y : x = y -> ~(x < y).
proof: Proof. intros E. rewrite E. apply (irreflexivity (<)). Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.apartness