proposition: Lemma add_cardinal_2 : forall s x, ~In x s -> cardinal (add x s) = S (cardinal s).
proof: Proof. intros. do 2 rewrite cardinal_fold. change S with ((fun _ => S) x); apply fold_add with (eqA:=@Logic.eq nat); auto with *. congruence. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide