proposition: Lemma exercise5_3 X i j (I:= domain X) (n := cardinal I) (ssI := fun k => subsets_with_p_elements k I) (uH := fun H => unionb (restr X H)) (iH := fun H => intersectionb (restr X H)) (iuH := fun k => intersectionf (ssI k) uH) (uiH := fun k => unionf (ssI k) iH): fgraph X -> natp n -> natp i -> natp j -> (((i = j \/ j <> \0c) -> i +c j <=c csucc n -> sub (iuH i) (uiH j)) /\ (csucc n <=c i +c j -> (i = j \/ j <=c n) -> sub (uiH i) (iuH j))).
proof: Proof. move => fgX nN iN jN. split. move => spec le1 t hyp. case: (equal_or_not j \0c) => jnz. have i0: i = \0c by case: spec => // ->. move: hyp; rewrite /iuH /uiH /ssI jnz i0. have re: (restr X emptyset) = emptyset. apply /set0_P => z /funI_P [a []]; case; case. have ->: (subsets_with_p_elements \0c I) = singleton emptyset. apply set1_pr. by apply/Zo_P; rewrite cardinal_set0;split => //; apply/setP_P; fprops. move => z /Zo_P [_]; apply:card_nonempty. by rewrite setUf_1 setIf_1 /uH /iH re setUb_0 setIb_0. set A := Zo I (fun z => ~ inc t (Vg X z)); set B := I -s A. have AI: sub A I by apply : Zo_S. move: (cardinal_setC2 AI); rewrite -/n -/B. rewrite -(csum2cr A) -(csum2cl A) => eq1. have bp: forall z, inc z B -> inc t (Vg X z). move => z /setC_P [zI] /Zo_P h; ex_middle tv; case: h;split => //. move: (nN);rewrite eq1 => nN'. have caN:= (NS_in_suml (CS_cardinal A) nN'). have cbN :=(NS_in_sumr (CS_cardinal B) nN'). case: (NleT_el jN cbN) => jcb. have [C [CB cC]]: exists C, sub C B /\ cardinal C = j. move: jcb; rewrite -(card_nat jN) => jcb. move: (proj2 (eq_subset_cardP _ _) (cardinal_le_aux1 jcb)). by move =>/set_leP [C c1 /card_eqP/esym c2]; exists C. have CI: sub C I by move => s sC; move:(CB _ sC);move /setC_P => []. apply /setUf_P; exists C. by apply/ Zo_P; split => //; apply/setP_P. apply /setIb_P. apply/domain_set0P;aw; apply /nonemptyP => ce. by move: cC; rewrite ce cardinal_set0; apply:nesym. by aw;move => l lC; rewrite LgV//; apply: bp; apply: CB. have: n <c cardinal A +c j. rewrite eq1; rewrite csumC (csumC _ j); apply:csum_Mlteq => //. move /(cleSltP nN) => le2. move: (cleT le1 le2); rewrite csumC (csumC _ j) => eq2. move:(csum_le2l jN iN caN eq2) => icA. have [C CB cC]: exists2 C, sub C A & cardinal C = i. move: icA; rewrite -(card_nat iN) => icA. move: (proj2 (eq_subset_cardP _ _) (cardinal_le_aux1 icA)). by move => /set_leP [C c1 /card_eqP /esym c2]; exists C. have CI: sub C I by move => s sC; move:(CB _ sC); apply: AI. have dsi:inc C (ssI i) by apply /Zo_i => //; apply /setP_P. move:(setIf_hi hyp dsi)=> /setUb_P [y]; rewrite restr_d. by move => yC; rewrite LgV//; move: (CB _ yC) => /Zo_P []. move => le hij. move => t /setUf_P [y pa pb]; apply /setIf_P. case: hij => jn; first by rewrite - jn; exists y. have kN:= (NS_le_nat jn nN). rewrite /ssI; apply /nonemptyP => he. move:(esym (card_p_subsets nN kN (refl_equal n))); rewrite he. rewrite cardinal_set0; exact: (binom_pr3 nN kN jn). move => z /Zo_P[/setP_P szi cz]. move /Zo_P:pa => [/setP_P syi cy]. case: (emptyset_dichot (y \cap z)) => di. move: (sub_smaller (setU2_12S syi szi)); rewrite (csum2_pr5 di). rewrite -(csum2cr y) cz -(csum2cl y) cy -/n. move => le1; case: (cleNgt (cleT le le1) (cltS nN)). move: di => [l /setI2_P [jz jy]]. apply/setUf_P; exists l;aww. have jr: inc l (domain (restr X y)) by aw. move: (setIf_hi pb jr); rewrite !LgV//. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)