proposition: Lemma nz2: 2 != 0 :> L.
proof: Proof. apply/eqP=> char2; apply: conj_nt => e; apply/eqP/idPn=> eJ. have opp_id x: - x = x :> L. by apply/esym/eqP; rewrite -addr_eq0 -mulr2n -mulr_natl char2 mul0r. have{} char2: 2%N \in [char L] by apply/eqP. without loss{eJ} eJ: e / conj e = e + 1. move/(_ (e / (e + conj e))); apply. rewrite fmorph_div rmorphD /= conjK -{1}[conj e](addNKr e) mulrDl. by rewrite opp_id (addrC e) divff // addr_eq0 opp_id. pose a := e * conj e; have aJ: conj a = a by rewrite rmorphM /= conjK mulrC. have [w Dw] := @solve_monicpoly _ 2%N (nth 0 [:: e * a; - 1]) isT. have{} Dw: w ^+ 2 + w = e * a. by rewrite Dw !big_ord_recl big_ord0 /= mulr1 mulN1r addr0 subrK. pose b := w + conj w; have bJ: conj b = b by rewrite rmorphD /= conjK addrC. have Db2: b ^+ 2 + b = a. rewrite -Frobenius_autE // rmorphD addrACA Dw /= Frobenius_autE -rmorphXn. by rewrite -rmorphD Dw rmorphM /= aJ eJ -mulrDl -{1}[e]opp_id addKr mul1r. have /eqP[] := oner_eq0 L; apply: (addrI b); rewrite addr0 -{2}bJ. have: (b + e) * (b + conj e) == 0. rewrite mulrDl 2![_ * (b + _)]mulrDr -/a. rewrite addrA addr_eq0 opp_id (mulrC e) -addrA. by rewrite -mulrDr eJ addrAC -{2}[e]opp_id subrr add0r mulr1 Db2. rewrite mulf_eq0 !addr_eq0 !opp_id => /pred2P[] -> //. by rewrite {2}eJ rmorphD rmorph1. 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)