proposition: Lemma left_right_not_compat : forall v v' d k k' b1 b2, search_tree (bnode k' d b1 b2) -> occ v k b1 -> occ v' k b2 -> False.
proof: Proof. inversion_clear 1; intros. destruct H2, H3. specialize (H2 _ _ H); specialize (H3 _ _ H4). generalize (M.lt_trans _ _ _ H2 H3). intros; now apply M.lt_irreflexive with k. Qed.
imports: Relations List ZArith Arith