proposition: Theorem gro: forall (i j: key) (m: t A), i <> j -> find i (remove j m) = find i m.
proof: Proof. induction i; intros; destruct j; destruct m; try rewrite (rleaf (xI j)); try rewrite (rleaf (xO j)); try rewrite (rleaf 1); auto; destruct m1; destruct o; destruct m2; simpl; try apply IHi; try congruence; try rewrite (rleaf j); auto; try rewrite (gleaf i); auto. - cut (find i (remove j (Node m2_1 o m2_2)) = find i (Node m2_1 o m2_2)); [ destruct (remove j (Node m2_1 o m2_2)); try rewrite (gleaf i); auto | apply IHi; congruence ]. - destruct (remove j (Node m1_1 o0 m1_2)); simpl; try rewrite (gleaf i); auto. - destruct (remove j (Node m2_1 o m2_2)); simpl; try rewrite (gleaf i); auto. - cut (find i (remove j (Node m1_1 o0 m1_2)) = find i (Node m1_1 o0 m1_2)); [ destruct (remove j (Node m1_1 o0 m1_2)); try rewrite (gleaf i); auto | apply IHi; congruence ]. - destruct (remove j (Node m2_1 o m2_2)); simpl; try rewrite (gleaf i); auto. - destruct (remove j (Node m1_1 o0 m1_2)); simpl; try rewrite (gleaf i); auto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface