fact: Definition introspective {R : ringType} n k (p : {poly R}) := rmodp (p ^+ n) ('X^k - 1) == rmodp (p \Po 'X^n) ('X^k - 1).
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound