proposition: Lemma cardinal_set_of_increasing_functions4 r r' (n := cardinal (substrate r')) (p := cardinal (substrate r)): total_order r -> total_order r' -> finite_set (substrate r) -> finite_set (substrate r') -> cardinal (functions_incr r r') = binom ((n +c p) -c \1c) p.
proof: Proof. move=> tor tor' fsr fsr'. rewrite (functions_incr_nat_prop tor tor' fsr fsr') -/n -/p. have nN: natp n by move: fsr' => /NatP. have pN: natp p by move: fsr => /NatP. case: (equal_or_not n \0c) => nz; last first. move: (cpred_pr nN nz) => [qa qb]. rewrite qb (card_increasing_nat qa pN). rewrite (csum_Sn _ qa) - (cpred_pr4 (CS_succ _)) cpred_pr2; fprops. rewrite nz (Nsum0l pN). case: (equal_or_not p \0c) => pz. rewrite pz (cdiff_wrong cle_01) binom00. set qq:= (functions_incr_nat \0c \0c). move:empty_function_function => /functionsP xx. have efq: inc empty_function qq. by apply/(increasing_nat_prop NS0 NS0); split => // i j _ /clt0. have ->: qq = singleton empty_function. apply:(set1_pr efq) => z /(increasing_nat_prop NS0 NS0) /proj1. by rewrite functions_empty => /set1_eq. by rewrite cardinal_set1. move: (cpred_pr pN pz) => [ppN sp]. rewrite - (cpred_pr4 (CS_nat pN)) (binom_bad ppN pN (cpred_lt pN pz)). case: (emptyset_dichot (functions_incr_nat p \0c)). by move=> ->; apply: cardinal_set0. move=> [f /(increasing_nat_prop pN NS0) [/functionsP [ff sf tf]] _]. have : inc (cpred p) (source f). rewrite sf {2} sp; apply /(NleP); fprops. by move/ (Vf_target ff); rewrite tf => /in_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)