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