Require Import nat_trees.
Require Import search_trees.
Require Import Compare_dec.



Theorem sch :
 ∀ (p : nat) (t : nat_tree), search t → {occ t p} + {¬ occ t p}.
Proof.
simple induction t;
 [ intros s; right
 | intros n t1 hr1 t2 hr2 s; elim (le_gt_dec p n); intros h;
    [ elim (le_lt_eq_dec p n h); intros h';
       [ elim hr1; [ intro k; left | intro k; right | idtac ] | left ]
    | elim hr2; [ intro k; left | intro k; right | idtac ] ] ];
 auto with searchtrees v62.

 Hint Resolve search_l search_r go_left go_right: searchtrees.
 eauto with searchtrees v62.
 eauto with searchtrees v62.
 rewrite h'; eauto with searchtrees v62.
 unfold not in |- *; eauto with searchtrees v62.
 eauto with searchtrees v62.
Defined.