proposition: Theorem remove_spec1: forall (m: t A)(i: key), find i (remove i m) = None.
proof: Proof. induction m; simpl. - intros; rewrite rleaf. apply gleaf. - destruct i; simpl remove; rewrite gnode; simpl; auto. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)