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