`{Trichotomy 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 [E|[E|E]];auto. - intros E1;destruct (LT_EQ E1). - intros E1;destruct (GT_EQ E1). Qed.
Require Import HoTT.Classes.interfaces.canonical_names.