proposition: Lemma unif_part_nat (a b : R) (n : nat) (x : R) : (a <= x <= b) -> {i : nat | nth 0 (unif_part a b n) i <= x < nth 0 (unif_part a b n) (S i) /\ (S (S i) < size (unif_part a b n))%nat} + {nth 0 (unif_part a b n) (n) <= x <= nth 0 (unif_part a b n) (S n)}.
proof: Proof. move: (sorted_dec (unif_part a b n) 0 x) => Hdec Hx. have Hs : sorted Rle (unif_part a b n) ; [ apply unif_part_sort, Rle_trans with (r2 := x) ; intuition | move: (Hdec Hs) => {Hs} Hdec]. have Hx' : (head 0 (unif_part a b n) <= x <= last 0 (unif_part a b n)). by rewrite head_unif_part last_unif_part. case: (Hdec Hx') => {Hdec Hx'} [[i Hi]|Hi]. left ; by exists i. right ; rewrite size_mkseq /= in Hi ; intuition. by rewrite Nat.sub_0_r in H1. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy