proposition: Lemma if_eq_dec x y (B:Type)(b b':B) : (if eq_dec x y then b else b') = (match compare x y with Eq => b | _ => b' end).
proof: Proof. destruct eq_dec; elim_compare x y; auto; order. Qed.
imports: Bool Basics OrdersTac Orders