proposition: Lemma min_not_occ : forall (k : key) (v : data) (t : btree), min k t -> ~ occ v k t.
proof: Proof. unfold not in |- *; 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