proposition: Lemma deriv_1_deriv' : forall (x : subset I), ProjT1 diffF x [=] ProjT1 (Diffble_I_n_imp_deriv_n _ _ diffFn) x.
proof: Proof. intros. elim deriv_1_deriv; intros H H1. elim H1; intros H0 H2. simpl in H2. clear H0 H1. generalize (H2 (scs_elem _ _ x) (scs_prf _ _ x) (scs_prf _ _ x) (scs_prf _ _ x)). intro H0. eapply eq_transitive_unfolded. eapply eq_transitive_unfolded. 2: apply H0. apply csf_wd_unfolded. cut (scs_elem _ _ x [=] scs_elem _ _ x). case x; simpl in |- *; auto. algebra. apply csf_wd_unfolded. cut (scs_elem _ _ x [=] scs_elem _ _ x). case x; simpl in |- *; auto. algebra. Qed.
imports: CoRN.ftc.Differentiability