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