fact: Definition Nbar (p q m : nat) : {set 'I_((p * q) ^ m).+1} := [set inZp (p ^ ij.1 * q ^ ij.2) | ij: 'I_m.+1 * 'I_m.+1].
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound