proposition: Lemma deg2_poly_factor : p = ('X - r1%:P) * ('X - r2%:P).
proof: Proof. by rewrite [p](@deg2_poly_factor _ _ _ _ r)// -/a a1 !mulr1 ?scale1r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)