proposition: Lemma set_of_functions_sum_pr n h (intv:= fun h => (Nint h)) (sle:= fun n h => graphs_sum_le (intv h) n) (seq := fun n h => graphs_sum_eq (intv h) n) (A:= fun n h => cardinal (sle n h)) (B:= fun n h => cardinal (seq n h)): natp n -> natp h -> (A n h = B n (csucc h) /\ A n h = (binom (n +c h) n)).
proof: Proof. move=> nN hN. have AB: forall a b, natp a -> natp b -> A a b = B a (csucc b). move=> a b aN bN; rewrite /A /B /sle/seq; apply /card_eqP. move: (Nint_pr4 bN) => [p1 p2]. rewrite /intv -p1; apply: (set_of_functions_sum1 aN p2). split; first by apply: AB. have Hv: forall a b, natp a -> natp b -> A (csucc a) b = (B (csucc a) b) +c (A a b). move=> a b aN bN; rewrite /A/B /sle /seq. by rewrite - (set_of_functions_sum2 (intv b) aN). apply: set_of_functions_sum0. - move=> a aN; rewrite /A/sle; apply: set_of_functions_sum3. - move=> a aN;rewrite /A/sle. have ->: (intv \0c = emptyset). by rewrite /intv;apply: Nint_co00. apply: set_of_functions_sum4 =>//. - move=> a b aN bN. by rewrite (Hv _ _ aN (NS_succ bN)) -(AB _ _ (NS_succ aN) bN). - exact. - exact. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)