proposition: Theorem remove_spec2: forall (m: t A)(i j: key), i <> j -> find j (remove i m) = find j m.
proof: Proof. induction m; simpl; intros. - now rewrite rleaf. - destruct i; simpl; rewrite gnode; destruct j; simpl; trivial; try apply IHm1; try apply IHm2; congruence. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)