`{Trichotomy A R} `{Irreflexive A R} : forall a b : A, compare a b = EQ <-> a = b. Proof. unfold compare,tricho_compare. intros a b;destruct (trichotomy R a b) as [E1|[E1|E1]];split;auto. - intros E2;destruct (LT_EQ E2). - intros E2;rewrite E2 in E1. destruct (irreflexivity R _ E1). - intros E2;destruct (GT_EQ E2). - intros E2;rewrite E2 in E1. destruct (irreflexivity R _ E1). Qed.
Require Import HoTT.Classes.interfaces.canonical_names.