proposition: Lemma card_Nbar p q m : prime p -> 1 < q -> ~ is_power q p -> #|Nbar p q m| = m.+1 ^ 2.
proof: Proof. move=> pP q_gt1 pCq. have p_gt1 := prime_gt1 pP. rewrite card_imset=> [|/= [i1 j1] [i2 j2] /(congr1 val)]. by rewrite card_prod card_ord expnS expn1. rewrite /= !modn_small //; last 2 first. - by rewrite ltnS expnMn leq_mul // leq_exp2l // -ltnS. - by rewrite ltnS expnMn leq_mul // leq_exp2l // -ltnS. wlog i1Li2 : i1 i2 j1 j2 / i1 <= i2 => H. case: (leqP i1 i2) => [i1Li2|i2Li1]; first by apply H. by move=> Hi; apply/sym_equal/H; rewrite 1?ltnW. suff [H1 H2] : (i1 : nat, j1 : nat) = (i2 : nat, j2 : nat). by congr (_, _); apply: val_inj. move: (i1Li2) H; rewrite leq_eqVlt => /orP[/eqP<-|i1LEi2 /eqP]. move/eqP; rewrite eqn_pmul2l; last by rewrite expn_gt0 ltnW. by rewrite eqn_exp2l => // /eqP<-. rewrite -{1}(subnK i1Li2) addnC expnD -mulnA eqn_pmul2l; last first. by rewrite expn_gt0 prime_gt0. case: (leqP j2 j1) => [j1Lj2|j2Lj1]. rewrite -{1}(subnK j1Lj2) expnD eqn_pmul2r; last by rewrite expn_gt0 ltnW. move: j1Lj2; rewrite leq_eqVlt => /orP[/eqP<-|]. rewrite subnn expn0 eq_sym. move: i1LEi2; rewrite -subn_gt0; case: (_ - _)%N=> // k _. by rewrite expnS muln_eq1; case: (p) p_gt1 => // [] []. rewrite -subn_gt0 => j1j2_gt0 /eqP qE. case: pCq; apply: prime_is_power_exp j1j2_gt0 _ => //. by rewrite qE is_power_exp. have j1LEj2 : j1 <= j2 by rewrite ltnW. rewrite -[_ ^ _]mul1n -{1}(subnK j1LEj2) expnD mulnA. rewrite eqn_pmul2r; last by rewrite expn_gt0 ltnW. move: i1LEi2; rewrite -subn_gt0; case: (_ - _)%N => // k _. by rewrite expnS -mulnA eq_sym muln_eq1; case: (p) p_gt1 => // [] []. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound