proposition: Lemma Riemann_fine_unif_part : forall (f : R -> R -> R) (a b : R) (n : nat), (forall a b, a <= b -> a <= f a b <= b) -> a <= b -> seq_step (SF_lx (SF_seq_f2 f (unif_part a b n))) <= (b - a) / (INR n + 1) /\ pointed_subdiv (SF_seq_f2 f (unif_part a b n)) /\ SF_h (SF_seq_f2 f (unif_part a b n)) = a /\ last (SF_h (SF_seq_f2 f (unif_part a b n))) (SF_lx (SF_seq_f2 f (unif_part a b n))) = b.
proof: Proof. intros f a b n Hf Hab. assert (Hab' : 0 <= (b - a) / (INR n + 1)). apply Rdiv_le_0_compat. apply -> Rminus_le_0. apply Hab. apply INRp1_pos. unfold pointed_subdiv. rewrite SF_lx_f2. change (head 0 (unif_part a b n) :: behead (unif_part a b n)) with (unif_part a b n). split ; [|split ; [|split]]. - cut (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)). + induction (unif_part a b n) as [|x0 l IHl]. now intros _. intros H. destruct l as [|x1 l]. easy. change (seq_step _) with (Rmax (Rabs (x1 - x0)) (seq_step (x1 :: l))). apply Rmax_case. apply Req_le. rewrite (H 0%nat). now apply Rabs_pos_eq. apply ->Nat.succ_lt_mono. apply Nat.lt_0_succ. apply IHl. intros i Hi. apply (H (S i)). now apply ->Nat.succ_lt_mono. + rewrite size_mkseq. intros i Hi. rewrite !nth_mkseq. rewrite S_INR. unfold Rdiv. ring. apply SSR_leq. now apply Nat.lt_le_incl. now apply SSR_leq. - unfold pointed_subdiv. rewrite SF_size_f2. rewrite size_mkseq. intros i Hi. rewrite SF_ly_f2. rewrite nth_behead. apply Nat.lt_succ_r, SSR_leq in Hi. rewrite (nth_pairmap 0). change (nth 0 (0 :: unif_part a b n) (S i)) with (nth 0 (unif_part a b n) i). apply Hf. rewrite !nth_mkseq //. rewrite S_INR. lra. now apply ssrnat.leqW. by rewrite size_mkseq. - apply head_unif_part. - apply last_unif_part. rewrite size_mkseq ; by apply Nat.lt_0_succ. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy