proposition: Lemma set_of_functions_sum0 f: (forall a, natp a -> f \0c a = \1c) -> (forall a, natp a -> f a \0c = \1c) -> (forall a b, natp a -> natp b -> f (csucc a) (csucc b) = (f (csucc a) b) +c (f a (csucc b))) -> forall a b, natp a -> natp b -> f a b = (binom (a +c b) a).
proof: Proof. move=> p2 p3 p4. move=> a b aN bN; move: a aN b bN. apply: Nat_induction. by move=> b bN; rewrite (p2 _ bN) (Nsum0l bN) binom0. move=> n nN fnb b bN. rewrite (csum_Sn _ nN). move: b bN; apply: Nat_induction. have snN: natp (csucc n) by fprops. by rewrite (Nsum0r nN) (binom_nn snN) (p3 _ snN). move=> c cN fsn. have sc: natp (csucc c) by fprops. rewrite (p4 _ _ nN cN) (fnb _ sc) fsn. by rewrite - (csum_nS _ cN) (binomSnSm (NS_sum nN sc) nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)