proposition: Lemma deg2_poly_maxE : p.[- b / (2 * a)] = - delta / (4 * a).
proof: Proof. apply/eqP; rewrite [eqbRHS]mulNr -eqr_oppLR -hornerN -b2a. by rewrite deg2_poly_minE// deltaN coefN mulrN divrNN. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)