`{Compare A} : forall a b : A, a =? b = true -> a ?= b = EQ. Proof. unfold eqb,compare_eqb;simpl. intros a b. destruct (a ?= b);trivial;intros E;destruct (false_ne_true E). Qed.
Require Import HoTT.Classes.interfaces.canonical_names.