proposition: Lemma unif_part_S a b n : unif_part a b (S n) = a :: unif_part ((a * INR (S n) + b) / INR (S (S n))) b n.
proof: Proof. apply eq_from_nth with 0. by rewrite /= !size_map !size_iota. case => [ | i] Hi. by rewrite nth0 head_unif_part. change (nth 0 (a :: unif_part ((a * INR (S n) + b) / INR (S (S n))) b n) (S i)) with (nth 0 (unif_part ((a * INR (S n) + b) / INR (S (S n))) b n) i). rewrite /unif_part size_mkseq in Hi. rewrite /unif_part !nth_mkseq ; try by intuition. rewrite !S_INR ; field. rewrite -!S_INR ; split ; apply sym_not_eq, (not_INR 0), O_S. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy