proposition: Lemma power_freePn n : ~~ power_free n (up_log 2 n) -> exists m, exists2 k, 1 < k & n = m ^ k.
proof: Proof. elim: up_log => [|[|k] IH]. - case: n => [|[|n]] //= _; first by exists 0%N; exists 2%N. by exists 1%N; exists 2%N. - case: {IH}n => [|[|n]] //= _; first by exists 0%N; exists 2%N. by exists 1%N; exists 2%N. rewrite power_freeSS is_rootnE //. case: (n =P rootn k.+2 n ^ k.+2) => [-> _|_]. by exists (rootn k.+2 n); exists k.+2. by case: k IH. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound