proposition: Lemma nexp_apply : forall (p : RX) n x, (p[^]n) ! x [=] p ! x[^]n.
proof: Proof. intros. induction n as [| n Hrecn]. astepl ([1]:RX) ! x. astepl ([1]:R). algebra. astepl (p[*]p[^]n) ! x. astepl (p ! x[*](p[^]n) ! x). astepl (p ! x[*]p ! x[^]n). algebra. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational