proposition: Lemma canonical_form (a b c : R[i]) : a != 0 -> let d := b ^+ 2 - 4%:R * a * c in let r1 := (- b - sqrtc d) / 2%:R / a in let r2 := (- b + sqrtc d) / 2%:R / a in a *: 'X^2 + b *: 'X + c%:P = a *: (('X - r1%:P) * ('X - r2%:P)).
proof: Proof. move=> a_neq0 d r1 r2. rewrite !(mulrDr, mulrDl, mulNr, mulrN, opprK, scalerDr). rewrite [_ * _%:P]mulrC !mul_polyC !scalerN !scalerA -!addrA; congr (_ + _). rewrite addrA; congr (_ + _). rewrite -opprD -scalerDl -scaleNr; congr(_ *: _). rewrite ![a * _]mulrC !divfK // !mulrDl addrACA !mulNr addNr addr0. rewrite -opprD opprK -mulrDr -mulr2n. by rewrite -(mulr_natl (_^-1)) divff ?mulr1 ?pnatr_eq0. symmetry; rewrite -!alg_polyC scalerA; congr (_%:A). rewrite [a * _]mulrC divfK // /r2 mulrA mulrACA -invfM -natrM -subr_sqr. rewrite sqr_sqrtc sqrrN /d opprB addrC addrNK -2!mulrA. by rewrite mulrACA -natf_div // mul1r mulrAC divff ?mul1r. 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)