proposition: Lemma monic_canonical_form (b c : R[i]) : let d := b ^+ 2 - 4%:R * c in let r1 := (- b - sqrtc d) / 2%:R in let r2 := (- b + sqrtc d) / 2%:R in 'X^2 + b *: 'X + c%:P = (('X - r1%:P) * ('X - r2%:P)).
proof: Proof. by rewrite /= -['X^2]scale1r canonical_form ?oner_eq0 // scale1r mulr1 !divr1. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrint div ssrnum rat poly closed_field) mathcomp(polyrcf matrix mxalgebra tuple mxpoly zmodp binomial realalg) mathcomp(mxpoly)