proposition: Lemma insert_leaf : forall (n : key) (v : data), INSERT n v leaf (bnode n v leaf leaf).
proof: Proof. intro n; split; auto with searchtrees. intros p k H; inversion_clear H; auto with searchtrees. Qed.
imports: Relations List ZArith Arith