proposition: Lemma cardinal_set_of_increasing_functions5 p n: natp p -> natp n -> cardinal(functions_incr (Nint_cco \1c p)(Nint_cco \0c n)) = binom (n +c p) p.
proof: Proof. move => pN nN. move: (Ninto_wor \1c p) (Ninto_wor \0c n)=> [a1 a2][a3 a4]. move: (worder_total a1) (worder_total a3). set r := (Nint_cco \1c p); set r' := (Nint_cco \0c n) => pa pb. move: (card_Nint1c pN);rewrite /Nint1c - a2. rewrite -/r => r1. have pc: finite_set (substrate r) by apply /NatP; rewrite r1. move: (card_Nintc nN);rewrite /Nintc - a4. rewrite -/r' => r2. have pd: finite_set (substrate r') by apply /NatP; rewrite r2; fprops. move: (cardinal_set_of_increasing_functions4 pa pb pc pd). rewrite r1 r2 (csum_Sn _ nN) (Nsucc_rw (NS_sum nN pN)). by rewrite (cdiff_pr1 (NS_sum nN pN) NS1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)