proposition: Lemma lead_coef_poly n E : n > 0 -> E n.-1 != 0 -> lead_coef (\poly_(i < n) E i) = E n.-1.
proof: Proof. by case: n => // n _ nzE; rewrite /lead_coef size_poly_eq // coef_poly leqnn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)