proposition: Lemma expansion_prop6: natp (Vg g k').
proof: Proof. have k'n := expansion_prop4. have [bN kn _ [_ d v]] := Expg. have kd: (inc k' (domain g)) by rewrite d; apply/(NleP k'n); fprops. exact:(NS_lt_nat (v _ kd) bN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)