proposition: Lemma eqb_compare x y : (x =? y) = match compare x y with Eq => true | _ => false end.
proof: Proof. apply eq_true_iff_eq. rewrite eqb_eq, <- compare_eq_iff. now destruct compare. Qed.
imports: Bool Basics OrdersTac Orders