proposition: Lemma remove_neq_o : forall A m x y, ~ E.eq x y -> find y (remove x m) = @find A y m.
proof: Proof. intros. unfold find. apply F.remove_neq_o. intro H_eq. contradict H. apply X.index_inj in H_eq. assumption. Qed.
imports: Coq(ZArith) Coq(FMapInterface FMapPositive) Coq(FMapList FMapFacts) Coq(String Ascii List) StructTact(StructTactics StringOrders)