proposition: Theorem rel_prime_Zpower_r i p q : 0 <= i -> rel_prime p q -> rel_prime p (q^i).
proof: Proof. intros Hi Hpq; pattern i; apply natlike_ind; auto with zarith. - simpl. apply rel_prime_sym, rel_prime_1. - clear i Hi. intros i Hi Rec; rewrite Z.pow_succ_r; auto. apply rel_prime_mult; auto. Qed.
imports: ZArith_base ZArithRing Lia Zcomplements Zdiv Znumtheory Zpower