fact: Fixpoint aks_param_search n a k c := if c is c1.+1 then if (k %| n)%nat then nice k else if (a <= k) && (a <= order_modn k n) then good k else aks_param_search n a k.+1 c1 else bad.
imports: mathcomp(all_ssreflect)