proposition: Lemma Exercise5_10 n k (o1 := Nint_cco \1c k) (o2 := Nint_cco \1c n) (even_odd_fct := fun f => (forall x, inc x (source f) -> evenp x -> evenp (Vf f x)) /\ (forall x, inc x (source f) -> oddp x -> oddp (Vf f x))): natp n -> natp k -> cardinal (Zo (functions_sincr o1 o2) even_odd_fct) = binom ((n +c k) %/c \2c) k.
proof: Proof. move: NS0 => ns0 nN kN; set A := Zo _ _. set I1:= Nint1c k; set I2:= Nint1c n. move: (proj2 (Ninto_wor \1c n)); rewrite -/o2 -/(Nint1c n) -/I2 => sr2. move: (proj2 (Ninto_wor \1c k)); rewrite -/o1 -/(Nint1c k) -/I1 => sr1. pose EF f z := Yo (z = \0c) \0c (Vf f z). move: (NS_succ kN); set sk := csucc k; move => skN. have pa: forall f, inc f A -> forall i, i <> \0c -> i <c sk -> inc i (source f). move => f /Zo_P [] /Zo_P [] /functionsP [ff sf tf] _ _ i inz ik. rewrite sf sr1; apply /(Nint1cP kN); split => //. by apply /(cltSleP kN). have pa': forall f, inc f A -> forall i, inc i (source f) -> i <> \0c /\ i <c sk. move => f /Zo_P [] /Zo_P [] /functionsP [ff sf tf] _ _ i. rewrite sf sr1; move /(Nint1cP kN) => [p1 p2];split => //. by apply /(cltSleP kN). have pb: forall f, inc f A -> (forall i, i <c sk -> natp (EF f i)). move => f fa; move: (fa) => /Zo_P [] /Zo_P [] /functionsP [ff sf tf] _ _. move => i ik; rewrite /EF; Ytac iz; [fprops | move: (pa _ fa _ iz ik)=> isf]. move: (Vf_target ff isf); rewrite tf sr2; apply: (Nint_S). have pc: forall f, inc f A -> (forall i j, i <c j -> j <c sk -> (EF f i) <c (EF f j)). move => f fa i j ij jsk. have jnz: j <> \0c by move => jz; case: (clt0 (x := i)); ue. move: (pa _ fa _ jnz jsk) => jsf. move: (fa) => /Zo_P [] /Zo_P [p1 [p2 p3 [p4 p5 p6] p7]] _. move: (pb _ fa _ jsk);rewrite /EF; Ytac0 => p8; Ytac iz. apply /strict_pos_P1 => //; move: (Vf_target p4 jsf). by rewrite p6 sr2; move /(Nint1cP nN) => []. move: ij => [lij nij]. move: (pa _ fa _ iz (cle_ltT lij jsk)) jsf; rewrite p5 sr1 => qa qb. have aux: glt o1 i j by split => //; apply /Ninto_gleP. by move: (p7 _ _ aux) => [] /Ninto_gleP [_ _ aa] bb; split. have pd: forall f, inc f A -> forall x, inc x (source f) -> x <=c Vf f x. move => f fA. move: (strict_increasing_prop1 skN (pb f fA) (pc f fA)) => h x xsf. by move: (pa' _ fA _ xsf) => [p1 p2]; move: (h _ p2); rewrite /EF; Ytac0. case: (NleT_el kN nN) => lekn; last first. have -> : A = emptyset. apply /set0_P => f fA. move /Zo_P: (fA) => [] /Zo_P [] /functionsP [ff sf tf] _ _. have ksf: inc k (source f). rewrite sf sr1; apply /Nint1cP => //;split;fprops => kz. by case: (clt0 (x := n)); rewrite - kz. move: (Vf_target ff ksf); rewrite tf sr2; move/(Nint1cP nN) => [_ H]. case: (cltNge lekn (cleT (pd _ fA _ ksf) H)). rewrite cardinal_set0 binom_bad //; first by fprops. move: (csum_Mlteq kN lekn) => lt1. move: (cdivision (NS_sum nN kN) NS2 card2_nz). set q := ((n +c k) %/c \2c); set r := ((n +c k) %%c \2c). move => [s1 s2 [s3 s4]]. apply: (cprod_lt2l NS2 s1 kN). rewrite -(csum_nn k); apply: cle_ltT lt1; rewrite s3. apply: (Nsum_M0le r (NS_prod NS2 s1)). move: (NS_diff k nN) => nkN. move: (cdivision nkN NS2 card2_nz). set p := (n -c k) %/c \2c; set r := ((n -c k) %%c \2c). move => [pN rN [p1 p2]]. have ->: (n +c k) %/c \2c = p +c k. have aux:cdivision_prop (n +c k) \2c (p +c k) r. split; last by exact. rewrite (csumC p) cprodDr - csumA - p1 -(csum_nn k) - csumA. by rewrite (cdiff_pr lekn) csumC. by rewrite (proj1 (cquorem_pr (NS_sum nN kN) NS2 (NS_sum pN kN) rN aux)). pose EG f x := ((Vf f x) -c x) %/c \2c. rewrite -(cardinal_set_of_increasing_functions5 kN pN). set o3:= Nint_cco \0c p; rewrite -/o1. set I3 := Nintc p. have sr3: substrate o3 = I3 by apply: (proj2 (Ninto_wor \0c p)). set B := functions_incr o1 o3. apply /card_eqP. exists (Lf (fun f => (Lf (EG f) I1 I3)) A B); saw. have pe: forall f, inc f A -> [/\ (forall x, inc x (source f) -> Vf f x = x +c \2c *c (EG f x)), lf_axiom (EG f) I1 I3 & inc (Lf (EG f) I1 I3) B]. move => f fA. move : (fA) => /Zo_P [] /Zo_P [] /functionsP [ff sf tf] ff1 ff2. have qa: (forall i : Set, i <c sk -> EF f i <c (n -c k) +c sk). move =>i isk; rewrite /sk (csum_nS _ kN) csumC (cdiff_pr lekn). apply /(cltSleP nN); rewrite /EF; Ytac zi; first apply: (cle0n nN). move: (pa _ fA _ zi isk) => isf. by move: (Vf_target ff isf); rewrite tf sr2; move/(Nint1cP nN) => []. have qb:(forall x, inc x (source f) -> (Vf f x) -c x <=c n -c k). move: (strict_increasing_prop3 skN (pb f fA) (pc f fA) nkN qa) => h. move => x xsf. by move: (pa' _ fA _ xsf) => [p4 p5]; move: (h _ p5); rewrite /EF; Ytac0. have qc: forall x, inc x (source f) -> natp (Vf f x -c x). move => x xsf; exact: (NS_le_nat (qb _ xsf) nkN). have qd: forall x, inc x (source f) ->x +c (Vf f x -c x) = Vf f x. move => x xsf; exact(cdiff_pr (pd _ fA _ xsf)). have qe: forall x, inc x (source f) -> evenp ((Vf f x) -c x). move => x xsf; move:(qd _ xsf) => h; move:(qc _ xsf) => dN. have xN: natp x by move: xsf; rewrite sf sr1; apply: Nint_S. ex_middle od; have oi: oddp (Vf f x -c x) by split. case: (p_or_not_p (evenp x)) => evx. move: (proj1 ff2 x xsf evx) => evf. by move: (csum_of_even_odd evx oi); rewrite h ; move => []. have oix: oddp x by split. move: (proj2 ff2 x xsf oix) => [_ evf]. by move: (csum_of_odd oix oi); rewrite h. have qf: forall x, inc x (source f) -> Vf f x = x +c \2c *c (EG f x). by move => x xsf; rewrite - (qd _ xsf) (half_even (qe _ xsf)). have qg: forall x, inc x (source f) -> natp (EG f x). by move => x xsf; apply: (NS_quo); apply: qc. have qh: forall x, inc x I1 -> inc (EG f x) I3. rewrite - sr1 - sf => x xsf; suff: Vf f x -c x <=c \2c *c p. rewrite (half_even (qe _ xsf)) => h. apply /(NintcP pN). exact(cprod_le2l NS2 (qg _ xsf) pN card2_nz h). have aux: cardinalp (\2c *c p) by fprops. move: (qb _ xsf); rewrite p1; case: (clt2 p2) => ->; rewrite ? csum0r //. apply: (even_compare pN (qe _ xsf)). have qi: increasing_fun (Lf (EG f) I1 I3) o1 o3. red; aw; split => //. by move: (Ninto_wor \1c k) => [[]]. by move: (Ninto_wor \0c p) => [[]]. by saw; try ue; apply: lf_function. move => i j /Ninto_gleP [iI jI ij]; rewrite !LfV//; apply/Ninto_gleP; split => //. by apply: qh. by apply: qh. have isf: inc i (source f) by rewrite sf sr1. have jsf: inc j (source f) by rewrite sf sr1. move: (pa' _ fA _ isf) (pa' _ fA _ jsf) => [s1 s2][s3 s4]. move: (strict_increasing_prop2 skN (pb f fA) (pc _ fA) ij s4). rewrite /EF; Ytac0; Ytac0. rewrite (half_even (qe _ isf)) (half_even (qe _ jsf)). apply: (cprod_le2l NS2 (qg _ isf) (qg _ jsf) card2_nz). split; [exact | exact | apply /Zo_P;split => //;apply/functionsP;red;aw]. move: qi => [_ _[fh _ _] _]; split => //. apply: lf_bijective. by move => f fA;move: (pe _ fA) => [_ _]. move => u v uA vA sv; move: (pe _ uA) (pe _ vA) => [a1 e1 _][a2 e2 _]. move /Zo_P: uA => [] /Zo_P [] /functionsP [u1 u2 u3] _ _. move /Zo_P: vA => [] /Zo_P [] /functionsP [v1 v2 v3] _ _. apply: function_exten => //; try ue. move => i isu /=; rewrite (a1 _ isu). rewrite u2 - v2 in isu; rewrite (a2 _ isu); congr (_ +c (_ *c _)). rewrite v2 sr1 in isu; move: (f_equal (Vf^~ i) sv). by rewrite !LfV. move => y /Zo_P [] /functionsP [fy sy tg] incy. set f := Lf (fun i => i +c \2c *c (Vf y i)) I1 I2. have qa: lf_axiom (fun i : Set => i +c \2c *c Vf y i) I1 I2. move => i i1; move: (i1) => /(Nint1cP kN) [qa qb]. apply /(Nint1cP nN); split. move: (cpred_pr (NS_le_nat qb kN) qa) => [sa sb]. rewrite {1} sb (csum_Sn _ sa); apply: succ_nz. rewrite - (cdiff_pr lekn); apply: (csum_Mlele qb); rewrite p1. apply: cleT (Nsum_M0le r (NS_prod NS2 pN)). apply: (cprod_Mlele (cleR CS2)); apply /(NintcP pN). by rewrite -/I3- sr3 -tg; Wtac; rewrite sy sr1. have ff: function f by apply: lf_function. have eof: even_odd_fct f. have aux: forall x, inc x I1 -> evenp (\2c *c Vf y x). move => x x1; apply: even_double. have aux: inc (Vf y x) I3 by rewrite - sr3 - tg; Wtac; rewrite sy sr1. apply: (Nint_S aux). red; rewrite /f; aw; split => x xsf; rewrite LfV// => ex. exact: (csum_of_even ex (aux _ xsf)). rewrite csumC; exact (csum_of_even_odd (aux _ xsf) ex). have fa: inc f A. apply /Zo_P; split; last by exact. apply /Zo_P; split; first by rewrite/f; apply /functionsP;red;saw. rewrite /f; red;split;aw;trivial. by move: (Ninto_wor \1c k) => [[]]. by move: (Ninto_wor \1c n) => [[]]. by saw. move: incy => [_ _ _ s6]. move => i j [] q1; move: (s6 _ _ q1) => /Ninto_gleP [a1 a2 q7]. move /Ninto_gleP: q1 => [q1 q2 q3] q4; rewrite !LfV//. have [q5 q6]: i +c \2c *c Vf y i <c j +c \2c *c Vf y j. move: (NS_prod NS2 (Nint_S a1)) (NS_prod NS2 (Nint_S a2)) => a3 a4. rewrite (csumC i) (csumC j); move: (cprod_Mlele (cleR CS2) q7) => q8. apply: (csum_Mlelt a4 q8 (conj q3 q4)). split; [apply /Ninto_gleP;split => //; by apply: qa | done ]. exists f => //. move: (pe _ fa) => [sa sb sc]. symmetry;apply: function_exten; aw; trivial;try ue; first by apply: lf_function. move => i iI1 /=; aw; rewrite /EG /f /=; rewrite LfV// LfV//. have aux: inc (Vf y i) I3 by rewrite - sr3 - tg; Wtac; rewrite sy sr1. have iB: natp i by apply: (Nint_S iI1). have fiB: natp (Vf y i) by apply: (Nint_S aux). rewrite csumC (cdiff_pr1 (NS_prod NS2 fiB) iB). apply: (cdivides_pr4 NS2 fiB card2_nz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)