proposition: Lemma Zrelprime_nexp : forall (p q : Z_as_CRing) n, Zrelprime p q -> Zrelprime p (q[^]n).
proof: Proof. intros p q n; intro H. induction n. apply Zgcd_one_rht. rewrite <- nexp_Sn. apply Zrelprime_symm. apply Zrelprime_mult_elim_lft. apply Zrelprime_symm; assumption. apply Zrelprime_symm; assumption. Qed.
imports: CPoly_Degree CRing_Homomorphisms Qring Zring Qordfield RingClass CRingClass Zlcm Q_can nat_Q_lists RX_deg QX_ZX