proposition: Lemma unif_part_bound (a b : R) (n : nat) : unif_part a b n = rev (unif_part b a n).
proof: Proof. apply (@eq_from_nth R 0) ; rewrite ?size_rev ?size_mkseq => // ; move => i Hi ; apply SSR_leq in Hi. rewrite nth_rev ?SSR_minus ?size_mkseq. 2: now apply SSR_leq. rewrite ?nth_mkseq. 3: now apply SSR_leq. rewrite minus_INR ?S_INR => // ; field. apply Rgt_not_eq, INRp1_pos. apply SSR_leq, INR_le ; rewrite ?S_INR minus_INR ?S_INR => //. apply Rminus_le_0 ; ring_simplify. apply pos_INR. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy