proposition: Lemma cardinal_Add_In: forall m m' x e, In x m -> Add x e m m' -> cardinal m' = cardinal m.
proof: Proof. assert (forall k e m, MapsTo k e m -> Add k e (remove k m) m) as remove_In_Add. { intros. unfold Add. intros. rewrite F.add_o. destruct (F.eq_dec k y). - apply find_1. rewrite <-MapsTo_m; [exact H|assumption|reflexivity|reflexivity]. - rewrite F.remove_neq_o by assumption. reflexivity. } intros. assert (Equal (remove x m) (remove x m')). { intros y. rewrite 2!F.remove_o. destruct (F.eq_dec x y). reflexivity. unfold Add in H0. rewrite H0. rewrite F.add_neq_o by assumption. reflexivity. } apply Equal_cardinal in H1. rewrite 2!cardinal_fold. destruct H as (e' & H). rewrite fold_Add with (eqA:=eq) (m1:=remove x m) (m2:=m) (k:=x) (e:=e'); try now (compute; auto). rewrite fold_Add with (eqA:=eq) (m1:=remove x m') (m2:=m') (k:=x) (e:=e); try now (compute; auto). rewrite <- 2!cardinal_fold. congruence. apply remove_1. reflexivity. apply remove_In_Add. apply find_2. unfold Add in H0. rewrite H0. rewrite F.add_eq_o; reflexivity. apply remove_1. reflexivity. apply remove_In_Add. assumption. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface