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