proposition: Lemma Exercise5_3a E n p k (X := Zo (\Po E \times \Po E) (fun z => [/\ cardinal (P z) = k, cardinal (Q z) = p -c cardinal (P z) & sub (Q z) (E -s P z)])): natp n -> natp p -> k <=c p -> cardinal E = n -> cardinal X = Exercise5_3V n p k.
proof: Proof. move => nN pN lkp ce. set F1 := subsets_with_p_elements k E. pose phi := Lf P X F1. have sp: X = source phi by rewrite /phi; aw. have tp: F1 = target phi by rewrite /phi; aw. have kN: natp k by apply (NS_le_nat lkp pN). symmetry; rewrite/Exercise5_3V. rewrite - (card_p_subsets nN kN ce) -/F1 tp sp. have lfa: lf_axiom P X F1. by move => t /Zo_P [] /setX_P [pa pb pc] [pd _ _]; apply: Zo_i. have fphi: function phi by apply: lf_function. symmetry;apply:(shepherd_principle fphi). move => x; rewrite - tp => xf. set K := Vfi1 _ _. move: (xf) => /Zo_P [] /setP_P xe cx. have nkN: natp (n -c k) by fprops. have pkN: natp (p -c k) by fprops. have fse: finite_set E by apply/NatP; rewrite ce. have cdx:cardinal (E -s x) = n -c k by rewrite (cardinal_setC4 xe fse) cx ce. rewrite - (card_p_subsets nkN pkN cdx). apply /card_eqP. set K0 := (subsets_with_p_elements (p -c k) (E -s x)). exists (Lf Q K (subsets_with_p_elements (p -c k) (E -s x))); saw. have k0p: forall y, inc y K <-> [/\ inc y (\Po E \times \Po E), P y = x & inc (Q y) K0]. move =>t; apply: (iff_trans (iim_fun_set1_P x fphi t)). rewrite - sp /phi; split. move => [tk]; rewrite LfV// => pt. move: tk => /Zo_P [te [p1 p2 p3]];split => //; apply/Zo_P. by rewrite -p1;split => //; apply /setP_P; rewrite pt. move => [p1 p2 p3]; suff: inc t X by move =>h; rewrite LfV. by move/ Zo_P: p3 => [] /setP_P sa sb; apply/ Zo_P; rewrite p2 cx. apply: lf_bijective. by move => t /k0p [_ _]. move => u v /k0p [u1 pu _]/k0p [v1 pv _] sv. by rewrite - (setX_pair u1) - (setX_pair v1) pu pv sv. move => y yk0; exists (J x y); aw; trivial;apply /k0p; saw. apply: setXp_i => //; apply /setP_P => //. by move /Zo_P: yk0 => [] /setP_P h _ t ty; move /setC_P: (h _ ty) => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)