proposition: Lemma value_b f: inc f dexpansions -> value f = csumb (size f) (fun i => (Vf f i) *c (\2c ^c i)).
proof: Proof. move => ha; move: (size_p ha) =>[hb hc _]. rewrite /value {1}/csumb; set g := Lg _ _. have qa: sub (size f) (domain g). by rewrite /g; aw; trivial; apply: NS_inc_nat. have qb:(forall i, inc i (domain g -s (size f)) -> Vg g i = \0c). rewrite /g;aw => i /setC_P[iN id]; rewrite LgV//. have ->: Vf f i = \0c. by apply: hc => //;case: (NleT_el hb iN) => // /(NltP hb). by rewrite cprod0l. rewrite (csum_zero_unit qa qb) /g; apply: csumb_exten => i ii; rewrite LgV//. apply:(NS_inc_nat hb ii). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)