proposition: Lemma Derivative_n_unique : forall n F G H, Derivative_n n I pI F G -> Derivative_n n I pI F H -> Feq I G H.
proof: Proof. intros n F G H H0 H1. elim H0; intros incF H2. elim H2; intros incG derivFG. elim H1; intros incF' H3. elim H3; intros incH derivFH. FEQ. rename X into H4. apply Feq_imp_eq with (Compact (less_leEq _ _ _ (proper_compact_in_interval' _ _ _ _ (compact_compact_in_interval I pI x H4)))). apply Derivative_I_n_unique with n F. apply derivFG. simpl in |- *; Included. apply derivFH. simpl in |- *; Included. apply interval_compact_inc. apply iprop_compact_in_interval. Qed.
imports: CoRN.ftc.MoreIntervals