proposition: Lemma cardinal_setC4 E A: sub A E -> finite_set E -> cardinal (E -s A) = (cardinal E) -c (cardinal A).
proof: Proof. move => AE /NatP sN. have cc:= (cardinal_setC AE); rewrite - cc in sN. symmetry; rewrite - cc csumC;apply: cdiff_pr1. exact: (NS_in_sumr (CS_cardinal (E -s A)) sN). exact:(NS_in_suml (CS_cardinal A) sN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)