proposition: Lemma deg2_poly_factor : p = a *: ('X - r1%:P) * ('X - r2%:P).
proof: Proof. rewrite [p]deg2_poly_canonical//= -/a -/b -/c -/delta /r1 /r2. rewrite ![(- b + _) * _]mulrDl 2!polyCD 2!opprD 2!addrA !mulNr !polyCN !opprK. rewrite -scalerAl [in RHS]mulrC -subr_sqr -polyC_exp -[4]/(2 * 2)%:R natrM. by rewrite -expr2 -exprMn [in RHS]exprMn exprVn r_sqrt_delta. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)