proposition: Lemma expansion_exists1 a k: natp k -> natp a -> a <c (b ^c k) -> exists f, expansion_of f b k a.
proof: Proof. move=> kN; move: k kN a. apply: Nat_induction. rewrite cpowx0 => c cN c1. exists (Lg emptyset (fun _ => \0c)); hnf; saw. split;fprops; split; fprops. by aw. by aw; move=> i /in_set0. rewrite /expansion_value/csumb; aw; rewrite csum_trivial; aw; trivial. by move: c1; rewrite - succ_zero; move / (cltSleP NS0) => /cle0 ->. move=> n nN pn c cN cp. set (b0:= b ^c n). have b0N: natp b0 by rewrite /b0; fprops. have Bz: (b0 <> \0c). have [_ /nesym bnz]:=(clt_ltT clt_01 bp). apply: (cpow_nz bnz). move: (cdivision cN b0N Bz) => [qN rN [aux lt]]. rewrite /b0 in lt. move: (pn _ rN lt) => [f [ise ev]]. have p1: (b0 *c (c %/c b0)) <c (b0 *c b). have p2: ((b0 *c (c %/c b0)) <=c c). by rewrite {2} aux; apply: csum_M0le; fprops. have p3: natp (b0 *c (c %/c b0)) by fprops. rewrite /b0 - cpow_succ -/b0; fprops; apply:cle_ltT p2 cp. move: (cprod_lt2l b0N qN bN p1) => qb. move: (expansion_prop8 ise qN qb). set F:= (Lg _ _). move=> [s1 s2]; exists F;split => //. by rewrite s2 ev {3} aux csumC /b0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)