fact: Definition mup (x : L) (p : {poly L}) := [arg max_(n > (0 : 'I_(size p).+1) | ('X - x%:P) ^+ n %| p) n] : nat.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)