proposition: Lemma cardinal_2 : forall m m' x e, ~ In x m -> Add x e m m' -> cardinal m' = S (cardinal m).
proof: Proof. intros; do 2 rewrite cardinal_fold. change S with ((fun _ _ => S) x e). apply fold_Add with (eqA:=eq); compute; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface