proposition: Lemma factoring_out_prime p x : prime p -> 0 < x -> exists k y, x = p ^ k * y /\ ~(p | y) /\ 0 <= k.
proof: Proof. intros pp xz. generalize xz. refine (Z_lt_induction (fun x => 0 < x -> exists k y : Z, x = p ^ k * y /\ ~ (p | y) /\ 0 <= k) _ x ltac:(lia)). clear x xz; intros x IHx xz. destruct (Zdivide_dec p x) as [ px | ? ]. 2:{ exists 0, x. split. rewrite Z.pow_0_r. lia. split. auto. lia. } pose proof prime_ge_2 p pp as p3. assert (0 < x / p). { apply Z.div_str_pos. split. lia. eapply Z.divide_pos_le; eauto. } destruct (IHx (x / p)) as (k & y & e & py & kz). - split. apply Z.div_pos; lia. apply Z.div_lt; lia. - auto. - exists (1 + k), y. split; auto. assert (k < 0 \/ 0 <= k) as [|] by lia. + rewrite Z.pow_neg_r in e; auto. lia. + rewrite Z.pow_add_r; try lia. rewrite <-Z.mul_assoc, <-e. replace (p ^ 1) with p by lia. apply Z_div_exact_2. lia. apply Zdivide_mod, px. + split; auto. lia. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)