proposition: Lemma compare_equal: forall s s', compare_fun s s' = Eq <-> equal s s' = true.
proof: Proof. induction s as [|l IHl o r IHr]; destruct s' as [|l' o' r']. - simpl. tauto. - unfold compare_fun, equal. case is_empty; intuition discriminate. - unfold compare_fun, equal. case is_empty; intuition discriminate. - simpl. rewrite <- 2andb_lazy_alt, 2andb_true_iff. rewrite <- IHl, <- IHr, <- compare_bool_Eq. clear IHl IHr. rewrite and_assoc. rewrite <- 2lex_Eq. reflexivity. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface