proposition: Lemma card_sincreasing_nat p n: natp p -> natp n -> cardinal (functions_sincr_nat p n) = binom n p.
proof: Proof. move=> pN nN. suff: bijection (Lf Imf (functions_sincr_nat p n) (subsets_with_p_elements p n)). move/card_bijection; aw; move ->. have nn: cardinal n = n by rewrite (card_card (CS_nat nN)). exact: (card_p_subsets nN pN nn). set src:= (functions_sincr_nat p n). set trg:= subsets_with_p_elements _ _. have ra f: inc f src -> injection f. move => /(sincreasing_nat_prop pN nN) [/functionsP[ff sf tf] fm]. split => //; rewrite sf => u v /(NltP pN) up /(NltP pN) vp sv. case: (cleT_ell (proj31_1 up)(proj31_1 vp)) => h. - done. - by case: (proj2(fm _ _ h vp)). - by case: (proj2(fm _ _ h up)). have ta: lf_axiom Imf src trg. move=> z zp. apply /Zo_P; rewrite (cardinal_range (ra _ zp)). move/(sincreasing_nat_prop pN nN): zp => [/functionsP[ff sf tf] _]. rewrite sf (card_card (CS_nat pN)) - tf; split => //; apply/setP_P. by apply: Imf_Starget. apply: lf_bijective =>//. move=> u v /(sincreasing_nat_prop pN nN) [/functionsP [fu su tu] um]. move => /(sincreasing_nat_prop pN nN) [/functionsP [fv sv tv] vm] si. apply: function_exten => //; try ue. rewrite su; move=> x /(NltP pN) xsu; ex_middle Wx. pose pr t := t <c p /\ Vf u t <> Vf v t. have prx: pr x by []. have xN: natp x. apply: (NS_lt_nat xsu pN). move: (least_int_prop xN prx); set y := least_ordinal _ _. move => [yN [yp ne] yl]. have ysu: inc y (source u) by rewrite su; apply/(NltP pN). have ysv: inc y (source v) by rewrite sv; apply/(NltP pN). have qa : Vf u y <c n by apply/(NltP nN); Wtac. have qb : Vf v y <c n by apply/(NltP nN); Wtac. case: (cleT_ee (proj31_1 qa)(proj31_1 qb)) => cuv. have: inc (Vf u y) (Imf v)by rewrite - si; apply: Imf_i. move/(Imf_P fv) =>[z]; rewrite sv => zp eqa. have qc : z <c p by apply/(NltP pN). case: (cleT_ell (proj31_1 yp)(proj31_1 qc)) => cyz. + by case: ne; rewrite eqa cyz. + by move:(vm y z cyz qc); rewrite - eqa => /cltNge; case. + move:(proj2 (um z y cyz yp)); rewrite eqa => ba. case: (cltNge cyz); exact: (yl z (NS_lt_nat cyz yN) (conj qc ba)). have: inc (Vf v y) (Imf u) by rewrite si; apply: Imf_i. move/(Imf_P fu) =>[z]; rewrite su => zp eqa. have qc : z <c p by apply/(NltP pN). case: (cleT_ell (proj31_1 yp)(proj31_1 qc)) => cyz. + by case: ne; rewrite eqa cyz. + by move:(um y z cyz qc); rewrite - eqa => /cltNge; case. + move:(proj2 (vm z y cyz yp)); rewrite eqa => /nesym ba. case: (cltNge cyz); exact: (yl z (NS_lt_nat cyz yN) (conj qc ba)). move => y/Zo_P [/setP_P stn cardy]. move: (Nat_order_wor) =>[or1 sr1]. have y1: sub y (substrate Nat_order) by rewrite sr1 => t /stn;apply: NS_inc_nat. move: (iorder_sr (proj1 or1) y1) (worder_total (induced_wor or1 y1)). set r := induced_order _ _ => sr tor. have fsi: finite_set (substrate r). by rewrite sr; apply:(sub_finite_set stn); apply: finite_set_nat. move:(finite_total_enum tor fsi); set f := the_ordinal_iso _. rewrite sr cardy; move =>[_ [bf sf tf] _ hb _]. have ff: function f by fct_tac. pose g := Lf (Vf f) p n. have ax: lf_axiom (Vf f) p n. move => t tp; apply: stn; Wtac. have fg: function g by apply: lf_function. have ig: y = Imf g. rewrite - tf - (surjective_pr0 (proj2 bf)); set_extens t. move/(Imf_P ff) =>[x xsf ->]; apply/ (Imf_P fg); rewrite /g; aw. by rewrite sf in xsf; ex_tac; rewrite LfV//. move/(Imf_P fg); rewrite/g; aw; move=> [x xn ->]. rewrite LfV//; apply: (Imf_i ff); ue. exists g => //. apply /(sincreasing_nat_prop pN nN); split. rewrite /g; apply/functionsP; saw. rewrite /g;move => i j lij ljp. have jp: inc j p by apply/(NltP pN). have ip: inc i p by apply/(NltP pN); apply: (clt_ltT lij ljp). rewrite !LfV//. by move:(hb _ _ lij ljp) => /iorder_gltP [_ _ [/Nat_order_leP [_ _ qc] sc]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)