proposition: Lemma compare_x_empty: forall a, is_empty a = true -> forall b, compare_fun b a = if is_empty b then Eq else Gt.
proof: Proof. setoid_rewrite <- compare_x_Leaf. intros. rewrite 2(compare_inv b), (compare_empty_x _ H). reflexivity. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface