proposition: Fact BGappendixC_inner_subproof : (p <= q)%N.
proof: Proof. have [y QP0y nUP0y] := nU_P0QP0. by apply: Einv_gt1_le_pq E_gt1; apply: BGappendixC3_Ediv nUP0y. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype choice ssrnat seq div fintype tuple finfun) mathcomp(bigop order ssralg finset prime binomial poly polydiv) mathcomp(fingroup morphism quotient automorphism action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator pgroup abelian frobenius) odd_order(BGsection1) mathcomp(matrix mxalgebra mxabelem vector falgebra fieldext galois) mathcomp(finfield ssrnum algC classfun character integral_char inertia)