proposition: Lemma interval_finite_subdiv (a b : R) (eps : posreal) : (a <= b) -> {l : seq R | head 0 l = a /\ last 0 l = b /\ forall i, (S i < size l)%nat -> nth 0 l i < nth 0 l (S i) <= nth 0 l i + eps}.
proof: Proof. move => Hab. suff Hn : 0 <= (b - a) / eps. set n : nat := nfloor ((b - a) / eps) Hn. case: (Req_EM_T (INR n) ((b - a) / eps)) => Hdec. set l : seq R := mkseq (fun k => a + INR k * eps) (S n). exists l. split. simpl ; rewrite /Rdiv ; ring. split. replace b with (a + INR n * eps). simpl. rewrite (last_map (fun k => a + INR k * eps) _ O) /=. rewrite (last_nth O) size_iota /=. case H : n => [ | m]. by simpl. by rewrite /nth -/(nth _ _ m) nth_iota. rewrite Hdec ; field. by apply Rgt_not_eq, eps. move => i Hi ; rewrite size_mkseq in Hi. split. rewrite ?nth_mkseq //. rewrite S_INR Rminus_lt_0 ; ring_simplify. by apply eps. elim: (S n) (S i) Hi => /= [ | m IH] ; case => /= [ | j] Hj //. by apply Nat.lt_irrefl in Hj. by apply Nat.nlt_0_r in Hj. by apply IH, Nat.succ_lt_mono. elim: (S n) (S i) Hi => /= [ | m IH] ; case => /= [ | j] Hj //. by apply Nat.nlt_0_r in Hj. by apply IH, Nat.succ_lt_mono. rewrite ?nth_mkseq //. rewrite S_INR Rminus_le_0 ; ring_simplify. by apply Rle_refl. elim: (S n) (S i) Hi => /= [ | m IH] ; case => /= [ | j] Hj //. by apply Nat.nlt_0_r in Hj. by apply IH, Nat.succ_lt_mono. elim: (S n) (S i) Hi => /= [ | m IH] ; case => /= [ | j] Hj //. by apply Nat.nlt_0_r in Hj. by apply Nat.nlt_0_r in Hj. by apply IH, Nat.succ_lt_mono. set l : seq R := rcons (mkseq (fun k => a + INR k * eps) (S n)) b. exists l. split. simpl ; rewrite /Rdiv ; ring. split. simpl ; by rewrite last_rcons. move => i Hi ; rewrite size_rcons size_mkseq in Hi ; apply (proj1 (Nat.lt_succ_r _ _)), le_S_n in Hi. split. rewrite ?nth_rcons size_mkseq. have H : ssrnat.leq (S i) (S n) = true. apply le_n_S in Hi ; elim: (S i) (S n) Hi => //= j IH ; case => //= [ | m] Hi. by apply Nat.nle_succ_0 in Hi. apply IH ; by apply le_S_n. case: (ssrnat.leq (S i) (S n)) (H) => // _. case H0 : (ssrnat.leq (S (S i)) (S n)) => //. rewrite ?nth_mkseq //. rewrite S_INR Rminus_lt_0 ; ring_simplify. by apply eps. apply (f_equal negb) in H0 ; simpl in H0. rewrite -ssrnat.leqNgt in H0. case H1 : (@eqtype.eq_op ssrnat_eqType (S i) (S n)) => //. rewrite ssrnat.eqSS /= in H1. replace i with n. rewrite nth_mkseq => //. move: Hdec ; rewrite /n /nfloor. case: nfloor_ex => {Hn l Hi H H0 H1} n Hn /= Hdec. rewrite Rplus_comm ; apply Rlt_minus_r. apply Rlt_div_r. by apply eps. case: Hn => Hn _ ; case: Hn => // Hn. elim: n i H1 {Hi H H0 l Hdec} => [ | n IH] ; case => [ | i] // H. apply f_equal, IH ; intuition. by rewrite ssrnat.eqn_leq H H0 in H1. rewrite ?nth_rcons size_mkseq. have H : ssrnat.leq (S i) (S n) = true. apply le_n_S in Hi ; elim: (S i) (S n) Hi => //= j IH ; case => //= [ | m] Hi. by apply Nat.nle_succ_0 in Hi. apply IH ; by apply le_S_n. case: (ssrnat.leq (S i) (S n)) (H) => // _. case H0 : (ssrnat.leq (S (S i)) (S n)) => //. rewrite ?nth_mkseq //. rewrite S_INR Rminus_le_0 ; ring_simplify. by apply Rle_refl. apply (f_equal negb) in H0 ; simpl in H0. rewrite -ssrnat.leqNgt in H0. case H1 : (@eqtype.eq_op ssrnat_eqType (S i) (S n)) => //. rewrite ssrnat.eqSS /= in H1. replace i with n. rewrite nth_mkseq => //. move: Hdec ; rewrite /n /nfloor. case: nfloor_ex => {Hn l Hi H H0 H1} n Hn /= Hdec. rewrite Rplus_assoc Rplus_comm ; apply Rle_minus_l. replace (INR n * eps + eps) with ((INR n + 1) * eps) by ring. apply Rle_div_l. by apply eps. by apply Rlt_le, Hn. elim: n i H1 {Hi H H0 l Hdec} => [ | n IH] ; case => [ | i] // H. apply f_equal, IH ; intuition. by rewrite ssrnat.eqn_leq H H0 in H1. apply Rdiv_le_0_compat. by apply Rminus_le_0 in Hab. by apply eps. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)