proposition: Lemma expansion_prop1 i: i <c k -> natp (Vg f i).
proof: Proof. move: Exp => [bN kn _ [_ d v]] /expansion_prop0P /v lt1. exact:(NS_lt_nat lt1 bN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)