proposition: Lemma expansion_restr1 f b k l: expansion f b k -> l <=c k -> expansion (restr f l) b l.
proof: Proof. move=> [bN kN b2 [fgf df vg]] lk. have lN:= NS_le_nat lk kN. split; fprops; split; aww => i idx; rewrite LgV//; apply: vg; rewrite df. by apply: (proj33 lk). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)