proposition: Lemma expansion_prop8_rev f b k x (h := Lg (csucc k) (fun i => variant \0c x (Vg f (cpred i)) i )): expansion f b k -> natp x -> x <c b -> (expansion h b (csucc k) /\ expansion_value h b = (expansion_value f b) *c b +c x).
proof: Proof. move => [bN kN b2 [fgf df vf]] xN xs. have skN:= (NS_succ kN). split. hnf;rewrite /h;split => //; aw; split; fprops => i ii; rewrite LgV//. rewrite /variant;Ytac iz => //. move/(NleP kN):ii => lij; move:(cpred_pr (NS_le_nat lij kN) iz) => [sa sb]. apply: vf; rewrite df; apply/(NltP kN);apply /(cleSltP sa); ue. move /(NleP kN): (cle0n kN) => zi. have ha:= (CS_nat xN). have hb: (Vg h \0c *c b ^c \0c) = x. by rewrite /h LgV //; aw; rewrite cpowx0 (cprod1r ha). rewrite /expansion_value df {1} /h Lgd (fct_sum_rec1 _ kN) hb //. congr (_ +c x). move: (kN) (cleR (CS_nat kN)); move: {- 3} k; apply: Nat_induction. move => _; rewrite /csumb !csum_trivial; aw; trivial. by rewrite cprod0l. move => n nN Hrec sa. have hc: inc (csucc n) (csucc k) by apply /(NleP kN). rewrite (induction_on_sum _ nN) (induction_on_sum _ nN). rewrite (Hrec (cleT (cleS nN) sa)) cprodDl - cprodA /h (LgV hc). by rewrite (variant_false _ _ (@succ_nz n)) (cpred_pr2 nN) (cpow_succ _ nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)