proposition: Lemma compdec_eq_eqb {T:Type} {c : CompDec T} : forall x y : T, x = y <-> eqb_of_compdec c x y = true.
proof: Proof. intros x y. destruct c as [TY [E HE] O C I]. unfold eqb_of_compdec. simpl. now rewrite HE. Qed.
imports: Bool OrderedType