proposition: Lemma finite_PET : K_is_large \/ exists z, (<< <<K; y>>; x>> = <<K; z>>)%VS.
proof: Proof. have [-> | /cyclic_or_large[|[a Dxa]]] := eqVneq x 0; first 2 [by left]. by rewrite addv0 subfield_closed; right; exists y. have [-> | /cyclic_or_large[|[b Dyb]]] := eqVneq y 0; first 2 [by left]. by rewrite addv0 subfield_closed; right; exists x. pose h0 (ij : 'I_a.+1 * 'I_b.+1) := x ^+ ij.1 * y ^+ ij.2. pose H := <<[set ij | h0 ij == 1%R]>>%G; pose h (u : coset_of H) := h0 (repr u). have h0M: {morph h0: ij1 ij2 / (ij1 * ij2)%g >-> ij1 * ij2}. by rewrite /h0 => [] [i1 j1] [i2 j2] /=; rewrite mulrACA -!exprD !expr_mod. have memH ij: (ij \in H) = (h0 ij == 1). rewrite /= gen_set_id ?inE //; apply/group_setP; rewrite inE [h0 _]mulr1. by split=> // ? ? /[!(inE, h0M)] /eqP-> /eqP->; rewrite mulr1. have nH ij: ij \in 'N(H)%g. by apply/(subsetP (cent_sub _))/centP=> ij1 _; congr (_, _); rewrite Zp_mulgC. have hE ij: h (coset H ij) = h0 ij. rewrite /h val_coset //; case: repr_rcosetP => ij1. by rewrite memH h0M => /eqP->; rewrite mul1r. have h1: h 1%g = 1 by rewrite /h repr_coset1 [h0 _]mulr1. have hM: {morph h: u v / (u * v)%g >-> u * v}. by do 2![move=> u; have{u} [? _ ->] := cosetP u]; rewrite -morphM // !hE h0M. have /cyclicP[w defW]: cyclic [set: coset_of H]. apply: field_mul_group_cyclic (in2W hM) _ => u _; have [ij _ ->] := cosetP u. by split=> [/eqP | -> //]; rewrite hE -memH => /coset_id. have Kw_h ij t: h0 ij = t -> t \in <<K; h w>>%VS. have /cycleP[k Dk]: coset H ij \in <[w]>%g by rewrite -defW inE. rewrite -hE {}Dk => <-; elim: k => [|k IHk]; first by rewrite h1 rpred1. by rewrite expgS hM rpredM // memv_adjoin. right; exists (h w); apply/eqP; rewrite eqEsubv !(sameP FadjoinP andP). rewrite subv_adjoin (subv_trans (subv_adjoin K y)) ?subv_adjoin //=. rewrite (Kw_h (0, inZp 1)) 1?(Kw_h (inZp 1, 0)) /h0 ?mulr1 ?mul1r ?expr_mod //=. by rewrite rpredM ?rpredX ?memv_adjoin // subvP_adjoin ?memv_adjoin. 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)