proposition: Lemma aks_param_search_goodP (n a k c r : nat) : aks_param_search n a k c = good r -> [/\ a <= r < k + c, a <= order_modn r n & forall j, k <= j <= r -> ~~ (j %| n)%nat].
proof: Proof. elim: c k => //= c IH k. have [//|ND] := boolP (_ %| _)%N. have [/andP[aLk aLo]|aLko] := boolP (_ && _). case => <-; split => // [| j]. by rewrite aLk addnS ltnS leq_addr. by rewrite -eqn_leq => /eqP<-. have {IH} := IH k.+1. case: aks_param_search => // r1 IH Hi. have := IH Hi; rewrite addnS => [] [H1 H2 H3]. split=> // j /andP[]. rewrite leq_eqVlt => /orP[/eqP<-//| kLj jLn1]. by apply: H3; rewrite kLj. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound