proposition: Lemma NbarP (p q m : nat) (x : 'I_ _) : 1 < p -> 1 < q -> reflect (exists (ij : 'I_m.+1 * 'I_m.+1) , x = (p ^ ij.1 * q ^ ij.2)%N :> nat) (x \in Nbar p q m).
proof: Proof. move=> p_gt1 q_gt1. apply(iffP imsetP) => [[[i j _ -> /=]]|[[i j ijE]]]. by exists (i, j); rewrite modn_small // ltnS expnMn leq_mul // leq_exp2l // -ltnS. exists (i, j) => //; apply/val_inj => /=. by rewrite modn_small // ltnS expnMn leq_mul // leq_exp2l // -ltnS. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound