proposition: Lemma deg2_poly_canonical : p = (('X + (b / 2)%:P)^+2 - (delta / 4)%:P).
proof: Proof. by rewrite [p]deg2_poly_canonical// -/a a1 scale1r expr1n !mulr1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)