proposition: Lemma aks_param_search_badP (n a k c : nat) : aks_param_search n a k c = bad -> (forall j , k <= j < k + c -> ~~(j %| n)%nat /\ order_modn j n < a).
proof: Proof. elim: c k => /= [k _ j|c IH k]; first by rewrite addn0; case: ltnP. have [//|ND] := boolP (_ %| _)%N. case: (leqP a k) => /= [aLk|kLa Hs j /andP[]] //. case: leqP => /= [aLo|oLa Hs j /andP[]] //. rewrite addnS leq_eqVlt => /orP[/eqP<- _|kLj jLkc]; first by split. by apply: (IH k.+1); rewrite // kLj. rewrite addnS leq_eqVlt => /orP[/eqP<- _|kLj jLkc]. split=> //. case: (k) kLa => [|k1 k1La]. by rewrite /order_modn andbF. apply: leq_trans k1La. apply: leq_trans (leq_order_totient _ _) _ => //. by apply: totient_leq. by apply: (IH k.+1); rewrite ?kLj. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound