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