proposition: Lemma char0_PET (q : {poly F}) : q != 0 -> root (q ^ iota) y -> [char F] =i pred0 -> exists n, let z := y *+ n - x in inFz z x /\ inFz z y.
proof: Proof. move=> nz_q qy_0 /charf0P charF0. without loss{nz_q} sep_q: q qy_0 / separable_poly q. move=> IHq; apply: IHq (make_separable nz_q). have /dvdpP[q1 Dq] := dvdp_gcdl q q^`(). rewrite {1}Dq mulpK ?gcdp_eq0; last by apply/nandP; left. have [n [r nz_ry Dr]] := multiplicity_XsubC (q ^ iota) y. rewrite map_poly_eq0 nz_q /= in nz_ry. case: n => [|n] in Dr; first by rewrite Dr mulr1 (negPf nz_ry) in qy_0. have: ('X - y%:P) ^+ n.+1 %| q ^ iota by rewrite Dr dvdp_mulIr. rewrite Dq rmorphM /= gcdp_map -(eqp_dvdr _ (gcdp_mul2l _ _ _)) -deriv_map Dr. rewrite dvdp_gcd derivM deriv_exp derivXsubC mul1r !mulrA dvdp_mulIr /=. rewrite mulrDr mulrA dvdp_addr ?dvdp_mulIr // exprS -scaler_nat -!scalerAr. rewrite dvdpZr -?(rmorph_nat iota) ?fmorph_eq0 ?charF0 //. rewrite mulrA dvdp_mul2r ?expf_neq0 ?polyXsubC_eq0 //. by rewrite Gauss_dvdpl ?dvdp_XsubCl // coprimep_sym coprimep_XsubC. have [r nz_r PETxy] := large_field_PET qy_0 sep_q. pose ts := mkseq (fun n => iota n%:R) (size r). have /(max_ring_poly_roots nz_r)/=/implyP: uniq_roots ts. rewrite uniq_rootsE mkseq_uniq // => m n eq_mn; apply/eqP; rewrite eqn_leq. wlog suffices: m n eq_mn / m <= n by move=> IHmn; rewrite !IHmn. move/fmorph_inj/eqP: eq_mn; rewrite -subr_eq0 leqNgt; apply: contraL => lt_mn. by rewrite -natrB ?(ltnW lt_mn) // charF0 -lt0n subn_gt0. rewrite size_mkseq ltnn implybF all_map => /allPn[n _ /= /PETxy]. by rewrite rmorph_nat mulr_natl; exists n. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop finset prime) mathcomp(binomial ssralg poly polydiv fingroup perm) mathcomp(morphism quotient gproduct finalg zmodp cyclic) mathcomp(matrix mxalgebra mxpoly polyXY vector falgebra) mathcomp(fieldext)