proposition: Lemma compare_x_Leaf: forall s, compare_fun s Leaf = if is_empty s then Eq else Gt.
proof: Proof. intros. rewrite compare_inv. simpl. case (is_empty s); reflexivity. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface