proposition: Lemma expansion_prop5: expansion (restr g k') b k'.
proof: Proof. have k'n :=expansion_prop4. have [bN kN b2 [fgf df vf]] := Expg. have dr: domain (restr g k') = k' by aw. split;fprops; split; fprops. by rewrite dr=> i ic; rewrite LgV//; apply: vf; rewrite df; apply: (proj33(cleS k'n)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)