proposition: Lemma FTtypeP_primes_mod_cases : [/\ odd ustar, p == 1 %[mod q] -> q %| ustar & p != 1 %[mod q] -> [/\ coprime ustar p.-1, ustar == 1 %[mod q] & forall b, b %| ustar -> b == 1 %[mod q]]].
proof: Proof. have ustar_mod r: p = 1 %[mod r] -> ustar = q %[mod r]. move=> pr1; rewrite -[q]card_ord -sum1_card /ustar predn_exp //. rewrite -(subnKC pgt2) mulKn // subnKC //. elim/big_rec2: _ => // i s1 s2 _ eq_s12. by rewrite -modnDm -modnXm pr1 eq_s12 modnXm modnDm exp1n. have ustar_odd: odd ustar. by apply: (can_inj oddb); rewrite -modn2 ustar_mod ?modn2 ?mFT_odd. split=> // [p1_q|p'1_q]; first by rewrite /dvdn ustar_mod ?modnn //; apply/eqP. have ustar_gt0: (ustar > 0)%N by rewrite odd_geq. have [p1_gt0 p_gt0]: (p.-1 > 0 /\ p > 0)%N by rewrite -(subnKC pgt2). have co_ustar_p1: coprime ustar p.-1. rewrite coprime_pi' //; apply/pnatP=> //= r pr_r. rewrite inE -subn1 -eqn_mod_dvd //= mem_primes pr_r ustar_gt0 => /eqP rp1. rewrite /dvdn ustar_mod // [_ == _]dvdn_prime2 //. by apply: contraNneq p'1_q => <-; apply/eqP. suffices ustar_mod_q b: b %| ustar -> b == 1 %[mod q]. by split; rewrite // ustar_mod_q. move=> b_dv_ustar; have b_gt0 := dvdn_gt0 ustar_gt0 b_dv_ustar. rewrite (prod_prime_decomp b_gt0) prime_decompE big_map /= big_seq. elim/big_rec: _ => // r s /(pi_of_dvd b_dv_ustar ustar_gt0). rewrite mem_primes -modnMml -modnXm => /and3P[pr_r _ r_dv_ustar]. suffices{s} ->: r = 1 %[mod q] by rewrite modnXm modnMml exp1n mul1n. apply/eqP; rewrite eqn_mod_dvd ?prime_gt0 // subn1. have ->: r.-1 = #|[set: {unit 'F_r}]|. rewrite card_units_Zp ?prime_gt0 ?pdiv_id //. by rewrite -[r]expn1 totient_pfactor ?muln1. have pq_r: p%:R ^+ q == 1 :> 'F_r. rewrite -subr_eq0 -natrX -(@natrB _ _ 1) ?expn_gt0 ?cardG_gt0 // subn1. rewrite -(divnK (dvdn_pred_predX p q)) -Fp_nat_mod //. by rewrite -modnMml (eqnP r_dv_ustar) mod0n. have Up_r: (p%:R : 'F_r) \is a GRing.unit. by rewrite -(unitrX_pos _ (prime_gt0 pr_q)) (eqP pq_r) unitr1. congr (_ %| _): (order_dvdG (in_setT (FinRing.unit 'F_r Up_r))). apply/prime_nt_dvdP=> //; last by rewrite order_dvdn -val_eqE val_unitX. rewrite -dvdn1 order_dvdn -val_eqE /= -subr_eq0 -val_eqE -(@natrB _ p 1) //=. rewrite subn1 val_Fp_nat //; apply: contraFN (esym (mem_primes r 1)). by rewrite pr_r /= -(eqnP co_ustar_p1) dvdn_gcd r_dv_ustar. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime binomial ssralg poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct center cyclic commutator gseries nilpotent) mathcomp(pgroup sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(ssrnum rat algC cyclotomic algnum) mathcomp(classfun character integral_char inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection7 PFsection8 PFsection9) odd_order(PFsection10 PFsection11 PFsection12)