proposition: Lemma deg2_poly_canonical : p = a *: (('X + (b / (2 * a))%:P)^+2 - (delta / (4 * a ^+ 2))%:P).
proof: Proof. rewrite pE sqrrD -!addrA scalerDr; congr +%R; rewrite addrA scalerDr; congr +%R. - rewrite -mulrDr -polyCD -!mul_polyC mulrA mulrAC -polyCM. by rewrite [a * _]mulrC mulrDl invfM -!mulrA mulVf// mulr1 -splitr. - rewrite [a ^+ 2]expr2 mulrA aa4 -polyC_exp -polyCB expr_div_n -mulrBl subKr. by rewrite scale_polyC mulrCA mulrACA aa4 mulrCA mulfV// mulr1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)