proposition: Fact conj_nt : ~ conj =1 id.
proof: Proof. have [i i2]: exists i : type, i ^+ 2 = -1. have [i] := @solve_monicpoly _ 2%N (nth 0 [:: -1 : type]) isT. by rewrite !big_ord_recl big_ord0 /= mul0r mulr1 !addr0; exists i. move/(_ i)/(congr1 CtoL); rewrite LtoC_K => iL_J. have/lt_geF/idP[] := @ltr01 cfType. rewrite -oppr_ge0 -(rmorphN1 CtoL). by rewrite -i2 rmorphXn /= expr2 -{2}iL_J -normCK exprn_ge0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq choice) mathcomp(div fintype path bigop finset prime order ssralg) mathcomp(poly polydiv mxpoly generic_quotient countalg) mathcomp(ssrnum closed_field ssrint archimedean rat intdiv) mathcomp(algebraics_fundamentals)