proposition: Lemma expe_bounded1 f k a: natp k -> expansion_ext_normal_of f (csucc k) a -> (\2c ^c k) <=c a.
proof: Proof. move => kN [[[ pa pb pc [pd pe pf]] pg] ph]. case: ph; [ by move:(@succ_nz k) | rewrite (cpred_pr2 kN) => ph ]. have kdf: inc k (domain f) by rewrite pe; apply: Nsucc_i. have aux:= (NS_lt_nat (pf _ kdf) NS3). pose h i := (Vg f i) *c (\2c ^c i). have le1: \2c ^c k <=c h k. rewrite /h cprodC; apply:(Nprod_M1le (NS_pow NS2 kN) (proj2 ph)). rewrite - pg /expansion_value pe (induction_on_sum h kN). apply:(cleT le1);apply /csum_Mle0; exact (proj32 le1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)