proposition: Lemma deg2_poly_min x : p.[- b / (2 * a)] <= p.[x].
proof: Proof. rewrite [p]deg2_poly_canonical ?pnatr_eq0// -/a -/b -/c /delta !hornerE/=. by rewrite ler_pM2l// lerD2r addrC mulNr subrr expr0n sqr_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)