proposition: Lemma power_freeP n m k : power_free n (up_log 2 n) -> n = m ^ k -> k = 1%N.
proof: Proof. move=> pH nE. have: k <= up_log 2 n. case: m pH nE => [|[|m]] //. - by case: k => // k; rewrite exp0n; case: n. - by rewrite exp1n; case: n => [|[|]]. move=> pH nE. have m_gt1 : 1 < m.+2 by []. rewrite -(leq_exp2l _ _ m_gt1). rewrite -nE. apply: leq_trans (up_logP _ (isT : 1 < 2)) _. rewrite leq_exp2r // up_log_gt0. by case: (n) pH => [|[|]]. elim: up_log pH => [|[|k1] IH]. - by case: k nE => //=; case: n => [|[|]]. - by case: {IH}k nE => [|[|k]] //=; case: n => [|[|]]. rewrite power_freeSS; case E: is_rootn => // pH. rewrite leq_eqVlt => /orP[/eqP kE |kLk1]; last by apply: IH. move: E; rewrite is_rootnE // [in rootn _ _]nE kE. by rewrite expnK // -kE -nE eqxx. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound