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