proposition: Lemma eq0_normc x : normc x = 0 -> x = 0.
proof: Proof. case: x => a b /= /eqP; rewrite sqrtr_eq0 le_eqVlt => /orP[|]; last first. by rewrite ltNge addr_ge0 ?sqr_ge0. by rewrite paddr_eq0 ?sqr_ge0 ?expf_eq0 //= => /andP[/eqP -> /eqP ->]. 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)