proposition: Lemma sqrtN1 : sqrtc (-1) = 'i.
proof: Proof. rewrite /sqrtc /= oppr0 eqxx [0^+_]exprS mulr0 addr0. rewrite exprS expr1 mulN1r opprK sqrtr1 subrr mul0r sqrtr0. by rewrite mul1r -mulr2n divff ?sqrtr1 // pnatr_eq0. 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)