proposition: Lemma tricho_compare_ok `{Trichotomy A R} `{Irreflexive A R} : forall a b : A, compare a b = EQ <-> a = b.
proof: 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.
imports: HoTT.Classes.interfaces.abstract_algebra