proposition: Lemma compare_eqb_eq `{Compare A} : forall a b : A, a =? b = true -> a ?= b = EQ.
proof: Proof. unfold eqb,compare_eqb;simpl. intros a b. destruct (a ?= b);trivial;intros E;destruct (false_ne_true E). Qed.
imports: HoTT.Classes.interfaces.abstract_algebra