proposition: Lemma interval_finite_subdiv_between (a b : R) (eps : posreal) (Hab : a <= b) : let l := proj1_sig (interval_finite_subdiv a b eps Hab) in forall i, (i < size l)%nat -> a <= nth 0 l i <= b.
proof: Proof. case: interval_finite_subdiv => l Hl /= i Hi. case: Hl => <- ; case => <- Hl. move: (fun i Hi => proj1 (Hl i Hi)) => {} Hl. rewrite -nth0 (last_nth 0). suff : forall n m, (n <= m)%nat -> (m < size l)%nat -> nth 0 l n <= nth 0 l m. move => {} Hl ; split. apply Hl ; by intuition. case: l Hi Hl => /= [ | x0 l] Hi Hl. by apply Nat.nlt_0_r in Hi. apply Hl ; by intuition. elim: l Hl {i Hi} => [ | x0 l IH] Hl n m Hnm Hm. by apply Nat.nlt_0_r in Hm. case: n m Hnm Hm => [ | n] m //= Hnm Hm. clear Hnm ; elim: m Hm => {IH} /= [ | m IH] Hm. by apply Rle_refl. apply Rle_trans with (nth 0 (x0 :: l) m). apply IH ; intuition. by apply Rlt_le, Hl. case: m Hnm Hm => /= [ | m] Hnm Hm. by apply Nat.nle_succ_0 in Hnm. apply IH ; try by intuition. move => i Hi. apply (Hl (S i)). by apply (proj1 (Nat.succ_lt_mono _ _)). Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)