proposition: Lemma last_unif_part x0 (a b : R) (n : nat) : last x0 (unif_part a b n) = b.
proof: Proof. rewrite (last_nth b) size_mkseq. replace (nth b (x0 :: unif_part a b n) (S (S n))) with (nth b (unif_part a b n) (S n)) by auto. rewrite nth_mkseq. rewrite S_INR ; field. by apply Rgt_not_eq, INRp1_pos. by []. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy