proposition: Lemma add_2 : forall m x y e e', ~ X.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
proof: Proof. intros m x y e e' He H; unfold PX.MapsTo in *. induction m as [|[z e''] m IHm]; simpl. - auto. - destruct X.compare as [Hlt|Heq|Hgt]; simpl. + auto with ordered_type. + apply InA_cons_tl; apply InA_cons in H; destruct H; [|assumption]. compute in H; intuition order. + apply InA_cons in H; destruct H; [now auto with ordered_type|]. apply InA_cons_tl; apply IHm, H. Qed.
imports: FMapInterface