proposition: Lemma go_left : forall (p : key) (v' : data), occ v' p (bnode n v t1 t2) -> Key.lt p n -> occ v' p t1.
proof: Proof. intros p v' H H0. case (occ_inv _ _ _ _ _ _ H). repeat simple destruct 1; absurd (Key.lt p n). rewrite H2; apply M.lt_irreflexive. assumption. simple destruct 1; trivial. intro H2; absurd (occ v' p t2). apply not_right. apply Key.lt_le_weak; assumption. auto. Qed.
imports: Relations List ZArith Arith