proposition: Lemma ct_compare_fun: forall a b c, ct (compare_fun a b) (compare_fun b c) (compare_fun a c).
proof: Proof. induction a as [|l IHl o r IHr]; intros s' s''. - destruct s' as [|l' o' r']; destruct s'' as [|l'' o'' r'']; ct. + rewrite compare_inv. ct. + unfold compare_fun at 1. case_eq (is_empty (Node l' o' r')); intro H'. * rewrite (compare_empty_x _ H'). ct. * unfold compare_fun at 2. case_eq (is_empty (Node l'' o'' r'')); intro H''. -- rewrite (compare_x_empty _ H''), H'. ct. -- ct. - destruct s' as [|l' o' r']; destruct s'' as [|l'' o'' r'']. + ct. + unfold compare_fun at 2. rewrite compare_x_Leaf. case_eq (is_empty (Node l o r)); intro H. * rewrite (compare_empty_x _ H). ct. * case_eq (is_empty (Node l'' o'' r'')); intro H''. -- rewrite (compare_x_empty _ H''), H. ct. -- ct. + rewrite 2 compare_x_Leaf. case_eq (is_empty (Node l o r)); intro H. * rewrite compare_inv, (compare_x_empty _ H). ct. * case_eq (is_empty (Node l' o' r')); intro H'. -- rewrite (compare_x_empty _ H'), H. ct. -- ct. + simpl compare_fun. apply ct_lex. * apply ct_compare_bool. * apply ct_lex; trivial. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface