proposition: Lemma Derivative_I_n_wdr : forall n F G H, Feq I G H -> Derivative_I_n Hab' n F G -> Derivative_I_n Hab' n F H.
proof: Proof. intro. induction n as [| n Hrecn]; intros F G H H0 H1. simpl in |- *; simpl in H1. apply Feq_transitive with G; assumption. elim H1; intros f' H2 H3. exists f'; auto. apply Hrecn with G; assumption. Qed.
imports: CoRN.ftc.Differentiability