proposition: Lemma expansion_restr2 f b k l: expansion f b k -> l <=c k -> (forall i, l <=c i -> i <c k -> Vg f i = \0c) -> expansion_value (restr f l) b = expansion_value f b.
proof: Proof. move=> ef lk p. pose g i := expansion_value (restr f i) b. move: (ef) => [bN kN b2 [fgf df vg]]. have ->: expansion_value f b = g k by rewrite /g -df restr_to_domain //. rewrite -/(g _). have H i: l <=c i -> i <c k -> g i = g (csucc i). move => lli lik; move: (NS_lt_nat lik kN) => iN. move/(cleSltP iN): (lik) => sik. move:(expansion_restr1 ef sik) => eF. rewrite /g (expansion_prop7 eF (CS_nat iN)). rewrite (double_restr _ (proj33 (cleS iN))) (restr_ev _ (Nsucc_i iN)). rewrite (p i lli lik) cprod0l csum0r //; apply: CS_cardinal. have H': forall i, natp i -> l <=c i -> i <=c k -> g l = g i. apply: Nat_induction; first by move => /cle0 ->. move => i iN h lsi /(cleSltP iN) lik. case: (cle_eqVlt lsi); [ by move -> | move/(cltSleP iN) => li]. by rewrite - (H _ li lik) (h li (proj1 lik)). by rewrite -/(g _ )(H' _ kN lk (cleR (proj32 lk))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)