proposition: Lemma csum_to_increasing6 n p: natp p -> natp n -> cardinal (graphs_sum_le (csucc p) n) = binom (csucc (n +c p)) (csucc p).
proof: Proof. move=> pN nN. rewrite - (csum_nS _ pN). rewrite - (card_increasing_nat nN (NS_succ pN)). apply /card_eqP. exists (Lf (fun y=> (csum_to_increasing_fct y n p)) (graphs_sum_le (csucc p) n) (functions_incr_nat (csucc p) (csucc n))). hnf;saw. by split; [apply: csum_to_increasing4 | apply: csum_to_increasing5]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)