proposition: Lemma unif_part_sort (a b : R) (n : nat) : a <= b -> sorted Rle (unif_part a b n).
proof: Proof. move => Hab ; apply sorted_nth => i Hi x0 ; rewrite ?size_mkseq in Hi ; rewrite ?nth_mkseq ?S_INR ; [ |apply SSR_leq ; intuition | apply SSR_leq ; intuition ]. apply Rminus_le_0 ; field_simplify ; [| apply Rgt_not_eq ; intuition] ; rewrite ?Rdiv_1 ; apply Rdiv_le_0_compat ; intuition. rewrite Rplus_comm ; by apply (proj1 (Rminus_le_0 _ _)). Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy