proposition: Lemma power_freeSS n k : power_free n k.+2 = if is_rootn k.+2 n then false else power_free n k.+1.
proof: Proof. by []. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound