proposition: Lemma nexp_ring_hom : forall R S (phi : RingHom R S) a n, phi (a[^]n) [=] phi a[^]n.
proof: Proof. intros; induction n; [apply rh_pres_unit|]. rewrite <- nexp_Sn, <- nexp_Sn; rewrite -> rh_pres_mult, IHn; reflexivity. Qed.
imports: CPoly_Degree CRing_Homomorphisms Qring Zring Qordfield RingClass CRingClass Zlcm Q_can nat_Q_lists RX_deg QX_ZX