fact: Definition aks n := let l := log2n n in if power_free n l then let v := aks_param n l in if v is nice k then n == k else if v is good k then fpoly_intro_range n k l else false else false.
imports: mathcomp(all_ssreflect)