proposition: Lemma Derivative_I_n_unique : forall n F G H, Derivative_I_n Hab' n F G -> Derivative_I_n Hab' n F H -> Feq I G H.
proof: Proof. intro. induction n as [| n Hrecn]; intros F G H H0 H1. simpl in H0, H1. unfold I in |- *; apply Feq_transitive with F. apply Feq_symmetric; assumption. auto. elim H0; intros g' H2 H3. elim H1; intros h' H4 H5. apply Hrecn with (PartInt g'). assumption. apply Derivative_I_n_wdl with (PartInt h'). 2: assumption. unfold I, Hab in |- *; apply Derivative_I_unique with F; assumption. Qed.
imports: CoRN.ftc.Differentiability