proposition: Lemma Exercise4_6e h K: natp h -> E46_hprop h -> inc K (free_subsets E46_order_r) -> (cardinal K) <=c (n +c h).
proof: Proof. move=> hN /Exercise4_6d aux free. set Z := K \cap (domain X). set Z1 := K \cap (domain Y). have ZX: sub Z (domain X) by apply: subsetI2r. have Z1Y: sub Z1 (domain Y) by apply: subsetI2r. move: Exercise4_6a => [[oR sR] rR]. case /free_subsetsP:free ;rewrite sR /E46_u; move=> pa pb. have uZ: K = Z \cup Z1. rewrite - (set_IU2r K (domain X) (domain Y)). by symmetry; apply /setI2id_Pl. have dj: disjoint Z Z1. apply: disjoint_pr => u ux uy; empty_tac1 u; saw. move: (csum2_pr5 dj); rewrite -uZ - csum2cr - csum2cl => cs. move:(proj42 Xpr) (proj42 Ypr) => cX cY. have cZN: natp (cardinal Z). have fsdX: finite_set (domain X) by hnf; rewrite cX; apply /NatP. by move: (sub_finite_set ZX fsdX) => /NatP. case: (NleT_ee cZN hN) => le1. move: (sub_smaller Z1Y) => aux1; move: (csum_Mlele le1 aux1). by rewrite - cs csumC cY. move:(NS_diff h cZN)(cdiff_pr le1);set r := (_ -c h); move=> rN phm. move: (sub_smaller ZX); rewrite cX => Zm. have c2:cardinal Z = r +c h by symmetry; rewrite csumC. rewrite cs c2 csumC csumA. apply: csum_Mlele; last by fprops. have c1: r <=c (m -c h). rewrite -phm in Zm; apply: (csum_le2l hN) => //; fprops. rewrite cdiff_pr //. by apply: cleT Zm; apply: csum_M0le; fprops. move: (aux _ _ c1 ZX c2) => [T [TdY cT etc]]. have di: disjoint Z1 T. apply: disjoint_pr => j jZ1 jT; move: (etc _ jT) => [i iZ le]. have iK: inc i K by rewrite uZ; apply /setU2_P; left. have jK: inc j K by rewrite uZ; apply /setU2_P; right. move: (pb i j iK jK le) => ij. by empty_tac1 i; rewrite ij. move:(csum2_pr5 di); rewrite - cY - cT csum2cr csum2cl => <-. apply: sub_smaller; move=> t; case /setU2_P => ta; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)