proposition: Lemma RM_1 : forall n:Z, RM n (Z_bnode n Z_leaf Z_leaf) Z_leaf.
proof: Proof. intros; apply rm_intro; auto with searchtrees. intros p H; elim (occ_inv H); auto with searchtrees. tauto. Qed.
imports: ZArith Extraction List