proposition: Lemma compare_inv: forall s s', compare_fun s s' = CompOpp (compare_fun s' s).
proof: Proof. induction s as [|l IHl o r IHr]; destruct s' as [|l' o' r']; trivial. - unfold compare_fun. case is_empty; reflexivity. - unfold compare_fun. case is_empty; reflexivity. - simpl. rewrite compare_bool_inv. case compare_bool; simpl; trivial; apply lex_Opp; auto. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface