proposition: Lemma seq_step_unif_part (a b : R) (n : nat) : seq_step (unif_part a b n) = Rabs ((b - a) / (INR n + 1)).
proof: Proof. assert (forall i, (S i < size (unif_part a b n))%nat -> (nth 0 (unif_part a b n) (S i) - nth 0 (unif_part a b n) i = (b - a) / (INR n + 1))%R). rewrite size_mkseq => i Hi. rewrite !nth_mkseq. rewrite S_INR /Rdiv /= ; ring. by apply SSR_leq, Nat.lt_le_incl. by apply SSR_leq. move: (eq_refl (size (unif_part a b n))). rewrite {2}size_mkseq. rewrite /seq_step ; elim: {2}(n) (unif_part a b n) H => [ | m IH] l //= ; destruct l as [ | x0 l] => //= ; destruct l as [ | x1 l] => //= ; destruct l as [ | x2 l] => //= ; intros. rewrite (H O). rewrite Rmax_comm /Rmax ; case: Rle_dec => // H1. contradict H1 ; by apply Rabs_pos. by apply ->Nat.succ_lt_mono; apply Nat.lt_0_succ. rewrite -(IH (x1::x2::l)) /=. rewrite (H O). rewrite (H 1%nat). rewrite Rmax_assoc. apply f_equal2 => //. rewrite /Rmax ; by case: Rle_dec. by apply ->Nat.succ_lt_mono; apply ->Nat.succ_lt_mono; apply Nat.lt_0_succ. by apply ->Nat.succ_lt_mono; apply Nat.lt_0_succ. now intros ; apply (H (S i)); apply ->Nat.succ_lt_mono. by apply eq_add_S. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy