proposition: Lemma factoring_out_prime_at_least_once p x : prime p -> 0 < x -> (p | x) -> exists k y, x = p ^ k * y /\ ~(p | y) /\ 1 <= k.
proof: Proof. intros pp xz px. destruct (factoring_out_prime p x pp xz) as (k & y & -> & py & kz). exists k, y; intuition. enough (k <> 0) by lia. intros ->. apply py. exact_eq px. f_equal. lia. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)