proposition: Lemma maj_not_occ : forall (k:key) (v:data) (t:btree), maj k t -> ~ occ v k t.
proof: Proof. intros k v t H H';destruct H; intros; absurd (Key.lt k k); auto. - apply M.lt_irreflexive. - eauto. Qed.
imports: Relations List ZArith Arith