proposition: Lemma bijective_complement n p E: natp n -> natp p -> p <=c n -> cardinal E = n -> bijection (Lf (complement E) (subsets_with_p_elements p E)(subsets_with_p_elements (n -c p) E)).
proof: Proof. move=> nN pN pn cE. apply: lf_bijective. - move=> z /Zo_P [] /setP_P ze p1; apply: Zo_i. apply /setP_P;apply: sub_setC. rewrite cardinal_setC4 ?cE ?p1 //; apply /NatP; ue. - move => u v /Zo_P [] /setP_P h1 _ /Zo_P [] /setP_P h2 _. by rewrite -{2}(setC_K h1) -{2}(setC_K h2) => ->. - move=> y /Zo_P [] /setP_P yE cy;exists (E -s y); last by rewrite (setC_K yE). apply: Zo_i; first by apply /setP_P; apply: sub_setC. have fse: finite_set E by apply /NatP; ue. rewrite (cardinal_setC4 yE fse) cy cE; apply: double_diff => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)