proposition: Lemma ex_diff_n_m : forall n m, (m <= n)%nat -> forall f x y, ex_diff_n f n x y -> ex_diff_n f m x y.
proof: Proof. assert (forall n f x y, ex_diff_n f (S n) x y -> ex_diff_n f n x y). induction n. simpl. intros f x y H; split; try apply H. intros f x y H. repeat (split; try apply H). apply IHn. apply H. apply IHn. apply H. intros n m H1 f x y Hn. induction n. - apply Nat.le_0_r in H1 as ->; exact Hn. - destruct (proj1 (Nat.lt_eq_cases _ _) H1) as [H2 | ->]; [| exact Hn]. now apply IHn; apply ->Nat.lt_succ_r in H2; [exact H2 |]; apply H; exact Hn. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive