proposition: Lemma expansion_exists3 a: natp a -> exists k f, expansion_normal_of f b k a.
proof: Proof. move=> aN; move:(expansion_exists2 aN) => [k [f [pa pb]]]. move: (pa) => [ha hb hc hd]. move:(hd) => [he hf hg]. pose prop l := l <=c k /\ forall i, l <=c i -> i <c k -> Vg f i = \0c. have pc: forall l, prop l -> expansion_of (restr f l) b l a. move => l [lk lp]. have lN := (NS_le_nat lk hb). split; last by rewrite (expansion_restr2 pa lk lp) pb. split => //; aw; split => //; fprops => i id; rewrite LgV//. move/(NltP lN):id => il; have ik := (clt_leT il lk). by apply: hg; rewrite hf; apply/(NltP hb). have neA: prop k by split; fprops => i ia /(cleNgt ia). case: (least_int_prop2 hb neA). by move/pc => h;exists \0c, (restr f \0c); split => //; left. set l := cpred _; move => [lN slA naA]. move: (pc _ slA) => h. have sa:= (Nsucc_i lN). exists (csucc l), (restr f (csucc l)); split => //; right. rewrite (cpred_pr2 lN); split; [by apply: succ_nz | rewrite LgV// => fz]. move:slA => [sc sd]. case naA; split; first exact:(cleT (cleS lN) sc). move => i i1 i2; case (equal_or_not l i) => eil; first by rewrite - eil. by apply: sd => //; apply/(cleSltP lN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)