proposition: Lemma Derivative_I_poly : forall p, Derivative_I Hab' (FPoly _ p) (FPoly _ (_D_ p)).
proof: Proof. induction p. apply Derivative_I_wdl with ([-C-] [0]). FEQ. apply Derivative_I_wdr with ([-C-] [0]). FEQ. Deriv. simpl. change (FPoly IR (cpoly_linear IR s p)) with (FPoly IR (s[+X*]p)). change (FPoly IR (cpoly_plus_cs IR p (cpoly_linear IR [0] (cpoly_diff IR p)))) with (FPoly IR (p[+]([0][+X*](_D_ p)))). apply Derivative_I_wdl with ([-C-] s{+}FId{*}(FPoly IR p)). repeat constructor. reflexivity. apply Derivative_I_wdr with ([-C-][0]{+}(FId{*}(FPoly IR (_D_ p)){+}[-C-][1]{*}(FPoly IR p))). repeat constructor. simpl. intros x _ _ _. change ([0][+](x[*](_D_ p)!x[+][1][*]p!x)[=] (p[+]([0][+X*](_D_ p)))!x). rewrite -> cpoly_lin. autorewrite with apply. rational. Deriv. Qed.
imports: CoRN.ftc.Derivative