proposition: Lemma deg2_poly_max x : p.[x] <= p.[- b / (2 * a)].
proof: Proof. by rewrite -lerN2 -!hornerN -b2a deg2_poly_min// coefN oppr_ge0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)