proposition: Lemma remove_1 : E.eq x y -> ~ In y (remove x m).
proof: Proof. intros; intro. generalize (mem_1 H0). rewrite mem_find. red in H. rewrite H. rewrite grs. intros; discriminate. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface