proposition: Lemma flip_coefficient : forall (p : RX) i, nth_coeff i (flip p) [=] [--] ( [--][1][^]i) [*]nth_coeff i p.
proof: Proof. intro p. elim p. simpl in |- *. algebra. intros c q. intros. elim i. simpl in |- *. ring. intros. simpl in |- *. astepl ( [--] (nth_coeff n (flip q))). astepl ( [--] ( [--] ( [--][1][^]n) [*]nth_coeff n q)). simpl in |- *. ring. Qed.
imports: CoRN.reals.IVT