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