proposition: Lemma inv_apply : forall (p : RX) x, ( [--]p) ! x [=] [--]p ! x.
proof: Proof. intros. pattern p in |- *. apply cpoly_induc. simpl in |- *. algebra. intros. astepl ( [--]c[+]x[*]( [--]p0) ! x). astepr ( [--](c[+]x[*]p0 ! x)). astepr ( [--]c[+][--](x[*]p0 ! x)). astepr ( [--]c[+]x[*][--]p0 ! x). algebra. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational