proposition: Lemma compare2eqb_spec x y : compare2eqb x y = true <-> x = y.
proof: Proof. unfold compare2eqb. case_eq (compare x y); simpl; intros e He; split; try discriminate; try (intros ->; elim (lt_not_eq _ _ e (eq_refl _))); auto. Qed.
imports: Bool OrderedType