proposition: Lemma rm_root_base_case : forall (n:Z) (t:Z_btree), search_tree (Z_bnode n Z_leaf t) -> RM n (Z_bnode n Z_leaf t) t.
proof: Proof. intros; apply rm_intro. - apply not_right with n Z_leaf; auto with searchtrees. reflexivity. - auto with searchtrees. - intros p H1; elim (occ_inv H1); intro H2. + right; auto. + case H2; intro. * absurd (occ p Z_leaf); auto with searchtrees. * now left. - apply search_tree_r with n Z_leaf; auto with searchtrees. Qed.
imports: ZArith Extraction List