proposition: Lemma card_increasing_nat n p: natp n -> natp p -> cardinal (functions_incr_nat p (csucc n)) = binom (n +c p) p.
proof: Proof. move=> nN pN; move: (NS_succ nN) => sN. set np := n +c p. have npN: natp np by rewrite /np; fprops. set Q1:= functions_incr_nat p (csucc n). set Q2:= functions_sincr_nat p np. move: (increasing_nat_prop pN sN); rewrite -/Q1 => HQ1P. move: (sincreasing_nat_prop pN npN); rewrite -/Q2 => HQ2P. pose subi f:= Lf (fun i=> (Vf f i) -c i) p (csucc n). have Hi0:forall f, inc f Q2 -> [/\ (forall i, i <c p -> natp (Vf f i)), (forall i j, i <c j -> j <c p -> (Vf f i) <c (Vf f j)) & (forall i, inc i p -> (i <=c (Vf f i)))]. move=> f /HQ2P [/functionsP [ff sf tf] sif]. have aux: (forall i, i <c p -> natp (Vf f i)). by move=> i /(NltP pN) ilp; apply:(NS_inc_nat npN); Wtac. by split => // i /(NltP pN); apply: strict_increasing_prop1. have Hi3:forall f, inc f Q2 -> lf_axiom (fun i => (Vf f i) -c i) p (csucc n). move=> f fQ2; move: (Hi0 _ fQ2) => [p1 p2 p3]. move: (strict_increasing_prop2 pN p1 p2) => p4. have p5: (forall i, i <c p-> (Vf f i) <c (n +c p)). move=> i ip. move: fQ2 => / HQ2P [ /functionsP [ff sf tf] vf]. have /(NltP npN) //: (inc (Vf f i) np). by rewrite -tf; Wtac; rewrite sf;apply/ (NltP pN). move=> i /(NltP pN) ip; apply /(NleP nN). apply:(strict_increasing_prop3 pN p1 p2 nN p5 ip). have Hi1:forall f, inc f Q2 -> inc (subi f) (functions p (csucc n)). move=> f fQ2;apply /functionsP; rewrite /subi; hnf;saw. by apply: lf_function; apply: Hi3. have Hi2:forall f, inc f Q2 -> inc (subi f) Q1. move=> f fQ2; apply/HQ1P. split; first by apply: Hi1. move: (Hi0 _ fQ2) (Hi3 _ fQ2) => [p1 p2 p3] ta. move => i j lij ljp. move/(NltP pN): (ljp) => qa; move/(NltP pN): (cle_ltT lij ljp) => qb. by rewrite /subi !LfV //; aw; apply (strict_increasing_prop2 pN p1 p2). set (G:= Lf subi Q2 Q1). have Hi4:function G by rewrite / G; apply: lf_function. pose addi f := Lf (fun i=> (Vf f i) +c i) p np. have pa:forall f, inc f (functions p (csucc n)) -> lf_axiom (fun i => (Vf f i) +c i) p np. move=> f /functionsP [ff sf tf] t tE1. have /(NleP nN) le1: (inc (Vf f t) (csucc n)) by Wtac. by move: tE1 => /(NltP pN) p1; apply /(NltP npN); apply: csum_Mlelt. have pa2: (forall f, inc f (functions p (csucc n)) -> inc (addi f) (functions p np)). move=> f fE; rewrite /addi; apply /functionsP;hnf;saw. by apply: lf_function; apply: pa. have pa3: forall f, inc f Q1 -> inc (addi f) Q2. move=> f /HQ1P [fe1e2 incf]; move: (pa _ fe1e2) => ax. apply /HQ2P; split; first by apply:pa2. move => i j lij ljp. move/(NltP pN): (ljp) => qa; move/(NltP pN): (clt_ltT lij ljp) => qb. rewrite/addi !LfV//. have aux: natp (Vf f j). apply: (NS_inc_nat sN); move /functionsP: fe1e2 => [ff sf tf]; Wtac. exact: (csum_Mlelt aux (incf _ _ (proj1 lij) ljp) lij). set (F:= Lf addi Q1 Q2). have ff: function F by apply: lf_function. have cGF: G \coP F by rewrite /G/F; saw. have cFG: F \coP G by rewrite /G/F; saw. have c1i: (G \co F = identity (source F)). apply: function_exten; aw;trivial; [fct_tac |apply: identity_f | | ]. by rewrite /G/F; aw. move => x xsf /=;rewrite (idV xsf) compfV //. rewrite corresp_s in xsf. have aQ2: inc (addi x) Q2 by apply: pa3. rewrite /F /G ! LfV// /addi/subi. move: (xsf) => /HQ1P [/functionsP [fx sx tx] icx]. apply: function_exten; aw =>//. apply: lf_function; apply: Hi3; apply: pa3 =>//. move: (Hi3 _ aQ2)=> ta2. move=> a aE1 /=; rewrite !LfV//. apply: cdiff_pr1; last by apply: (NS_inc_nat pN). apply: (NS_inc_nat sN);rewrite -tx//; Wtac. by apply: pa; apply /functionsP. have c2i: (F \co G = identity (source G)). apply: function_exten; [fct_tac | fprops | by aw | by rewrite /F/G; aw | ]. rewrite /G; aw => x xQ2. have qQ1: inc (subi x) Q1 by apply: Hi2. move: (xQ2) => /HQ2P [/functionsP [fx sx tx] icx]. rewrite idV// compfV // ?lf_source // /F ! LfV// /addi/subi. symmetry; apply: function_exten; aw; trivial. apply: lf_function; apply: pa; apply: Hi1=> //. have ta3:= (Hi3 _ xQ2). have ta2:=(pa _ (Hi1 _ xQ2)). rewrite sx => i isx; rewrite ! LfV // cdiff_rpr //. exact: (proj33 (Hi0 _ xQ2) i isx). move: (bijective_from_compose cGF cFG c1i c2i) => /proj31. move/card_bijection; rewrite /F; aw => ->. by rewrite card_sincreasing_nat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)