proposition: Fact take_poly_is_linear m : linear (take_poly m).
proof: Proof. by move=> k p q; rewrite take_polyD take_polyZ. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)