proposition: Lemma deg2_poly_minE : p.[- b / (2 * a)] = - delta / (4 * a).
proof: Proof. rewrite [p]deg2_poly_canonical ?pnatr_eq0// -/a -/b -/c -/delta !hornerE/=. rewrite [X in X^+2]addrC [in LHS]mulNr subrr expr0n add0r mulNr. by rewrite mulrC mulNr invfM mulrA mulfVK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)