proposition: Lemma flip_poly : forall (p : RX) x, (flip p) ! x [=] [--]p ! ( [--]x).
proof: Proof. intro p. elim p. intros. simpl in |- *. algebra. intros c q. intros. change ( [--]c[+]x[*] (cpoly_inv _ (flip q)) ! x [=] [--] (c[+][--]x[*]q ! ( [--]x))) in |- *. astepl ( [--]c[+]x[*][--] (flip q) ! x). astepl ( [--]c[+]x[*][--][--]q ! ( [--]x)). ring. Qed.
imports: CoRN.reals.IVT