proposition: Lemma exp_Mk_upper_bound (R : comRingType) k s n a (M : {set 'Z_k}) : Mk_spec R s M -> 1 < #|M| -> 1 < k -> 1 < n -> isnot_2power n -> a = up_log 2 n ^ 2 -> a <= order_modn k n -> s = (sqrtn (totient k) * (up_log 2 n))%N -> is_iexp R k s n -> n ^ (sqrtn #|M|) < 2 ^ (minn s #|M|).
proof: Proof. move=> HMk Mk_gt1 k_gt1 m_g1 nNP aE aLo sE nIN. set j := order_modn k n in aLo. set m := up_log 2 n in aE sE. have F1 : j <= #|M| by apply: is_iexpm_order. have F2 : #|M| <= totient k by apply: is_iexpm_totient. have F3 : m ^ 2 <= j by move: aLo; rewrite aE. apply: leq_trans (_ : (2 ^ m) ^ sqrtn (#|M|) <= _). rewrite ltn_exp2r; last first. by rewrite sqrtn_gt0 (leq_trans _ (_ : 2 <= _)). by have := up_logP n (isT : 1 < 2); rewrite leq_eqVlt (negPf nNP). case: (leqP s #|M|) => [sLM|MLs]. by rewrite -expnM leq_exp2l // sE mulnC leq_mul2r // orbC leq_sqrtn. rewrite -expnM leq_exp2l //. apply: leq_trans (_ : (sqrtn #|M|) ^ 2 <= _); last first. by have /andP[] := sqrtn_bound #|M|. rewrite expnS expn1 leq_mul2r // orbC. rewrite (leq_trans _ (_ : sqrtn j <= _)) //; last by apply: leq_sqrtn. by rewrite -[m]sqrnK leq_sqrtn . Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound