fact: Definition poly_order {R : ringType} (h p : {poly R}) (n : nat) : nat := if [pick i | rmodp (p^+ (i : 'I_n.+1).-1.+1) h == 1] is Some v then [arg min_(i < v | (rmodp (p^+ i.-1.+1) h == 1)) i].-1.+1 else 0.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)