proposition: Lemma irrefl_neq `{R : Relation A} `{!Irreflexive R} : forall x y, R x y -> x <> y.
proof: Proof. intros ?? E e;rewrite e in E. apply (irreflexivity _ _ E). Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.apartness