proposition: Theorem rel_prime_Zpower i j p q : 0 <= i -> 0 <= j -> rel_prime p q -> rel_prime (p^i) (q^j).
proof: Proof. intros Hi Hj H. apply rel_prime_Zpower_r; trivial. apply rel_prime_sym. apply rel_prime_Zpower_r; trivial. now apply rel_prime_sym. Qed.
imports: ZArith_base ZArithRing Lia Zcomplements Zdiv Znumtheory Zpower