proposition: Lemma le_imp_Diffble_I : forall m n : nat, m <= n -> forall F, Diffble_I_n Hab' n F -> Diffble_I_n Hab' m F.
proof: Proof. intros m n H F H0. induction n as [| n Hrecn]. cut (m = 0); [ intro | auto with arith ]. rewrite H1; simpl in |- *; tauto. elim (le_lt_eq_dec _ _ H); intro H2. 2: rewrite H2; assumption. apply Hrecn. auto with arith. elim H0; intros Hf Hf'. clear Hf' Hf H2 Hrecn H. generalize H0. generalize F. clear H0 F; induction n as [| n Hrecn]; intros. simpl in |- *; apply diffble_imp_inc. exact (Diffble_I_n_imp_diffble _ (Nat.lt_succ_diag_r 0) F H0). simpl in |- *. elim H0; intros Hf Hf'. exists Hf. apply Hrecn. assumption. Qed.
imports: CoRN.ftc.Differentiability