proposition: Lemma expansion_prop3: natp (expansion_value f b).
proof: Proof. rewrite /expansion_value; apply: finite_sum_finite. apply: expansion_prop2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)