proposition: Lemma eqp_take_drop n p q : take_poly n p = take_poly n q -> drop_poly n p = drop_poly n q -> p = q.
proof: Proof. by move=> tpq dpq; rewrite -[p](poly_take_drop n) -[q](poly_take_drop n) tpq dpq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)