proposition: Lemma not_left : forall (p : key) (v' : data), Key.le n p -> ~ occ v' p t1.
proof: Proof. intros p v' H; elim maj_l. unfold not in |- *; intros; absurd (Key.lt p n); eauto with searchtrees. apply M.le_not_lt; assumption. Qed.
imports: Relations List ZArith Arith