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; now 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. + assumption. Qed.
imports: Relations List ZArith Arith