proposition: Lemma NS_expe_val f k: expansion_ext f k -> natp (expansion_value f \2c).
proof: Proof. move =>[bN kN b2 [fgf df vf]]; apply: finite_sum_finite. hnf; rewrite /allf; aw; split. move=> i idf; rewrite LgV//; rewrite df in vf idf; move: (vf _ idf) => h. apply:(NS_prod (NS_lt_nat h bN) (NS_pow NS2 (NS_inc_nat kN idf))). by rewrite df; apply: finite_set_nat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)