proposition: Lemma rmax_leaf_leaf : forall n:Z, RMAX (Z_bnode n Z_leaf Z_leaf) Z_leaf n.
proof: Proof. intro n; split; auto with searchtrees. - intros p H; inversion_clear H; auto with searchtrees. + auto with zarith. + absurd (occ p Z_leaf); auto with searchtrees. + absurd (occ p Z_leaf); auto with searchtrees. - inversion_clear 1 ; auto with searchtrees. Qed.
imports: ZArith Extraction List