proposition: Lemma Q_Z_nexp : forall (p : Z_as_CRing) (q : positive) i, ((p#q)[^]i[*](q:Q_as_CRing)[^]i [=] p[^]i)%Q.
proof: Proof. intros p q. induction i. reflexivity. rewrite <- nexp_Sn, <- nexp_Sn, <- nexp_Sn. rewrite -> (mult_commutes _ (p#q)%Q). rewrite <- CRings.mult_assoc. rewrite -> (mult_commutes _ (p#q)%Q). rewrite -> (mult_commutes _ (q:Q_as_CRing)). rewrite -> CRings.mult_assoc. rewrite -> CRings.mult_assoc. rewrite -> IHi. rewrite (mult_commutes _ p). rewrite <- CRings.mult_assoc. apply (mult_wdr _ (inject_Z ((p:Z_as_CRing)[^]i)) ((q:Q_as_CRing)[*](p # q)%Q) p). simpl; unfold Qeq; simpl. case p. rewrite Zmult_0_l, Zmult_0_l; reflexivity. intro r; rewrite Zmult_1_r; rewrite Zmult_comm; reflexivity. intro r; rewrite Zmult_1_r; rewrite Zmult_comm; reflexivity. Qed.
imports: CPoly_Degree CRing_Homomorphisms Qring Zring Qordfield RingClass CRingClass Zlcm Q_can nat_Q_lists RX_deg QX_ZX