proposition: Lemma StepFun_bound {a b : R} (f : StepFun a b) : exists s : R, forall x, Rmin a b <= x <= Rmax a b -> f x <= s.
proof: Proof. case: f => /= f [lx [ly [Hsort [Hhead [Hlast [Hsize Hval]]]]]]; rename a into a0 ; rename b into b0 ; set a := Rmin a0 b0 ; set b := Rmax a0 b0 ; set Rl_max := fun x0 => fix f l := match l with | nil => x0 | h :: t => Rmax h (f t) end ; set f_lx := (fix app l := match l with | nil => nil | h :: t => f h :: app t end) lx ; set M_f_lx := Rl_max (f 0) f_lx ; set M_ly := Rl_max 0 ly. exists (Rmax M_f_lx M_ly) => x [Hx Hx']. rewrite /M_f_lx /f_lx ; case: lx Hsort Hhead Hlast Hsize Hval {f_lx M_f_lx}. move => _ _ _ H ; contradict H ; apply O_S. move => h l ; case: l h. move => h _ Ha Hb _ _ ; simpl in Ha, Hb. rewrite /a -Ha in Hx ; rewrite /b -Hb in Hx'. rewrite (Rle_antisym _ _ Hx Hx') /= ; apply Rle_trans with (2 := RmaxLess1 _ _) ; apply RmaxLess1. move => h l h' Hsort Hhead Hlast Hsize Hval. apply Rle_lt_or_eq_dec in Hx' ; case: Hx' => Hx'. have H : exists i : nat, (i < S (length l))%nat /\ (RList.pos_Rl (cons h' (h :: l)) i) <= x < (RList.pos_Rl (cons h' (h :: l)) (S i)). rewrite /a -Hhead in Hx ; rewrite /b -Hlast in Hx'. elim: l h' h Hx Hx' Hsort {Hhead Hlast Hsize Hval} => [| h'' l IH] h' h Hx Hx' Hsort ; simpl in Hx, Hsort. case: (Rlt_le_dec x h) => H. exists O ; intuition. exists O => /= ; intuition. case: (Rlt_le_dec x h) => H. exists O => /= ; intuition. have H0 : RList.ordered_Rlist (h :: h'' :: l). move => i Hi ; apply (Hsort (S i)) => /= ; apply (proj1 (Nat.succ_lt_mono _ _)), Hi. case: (IH _ _ H Hx' H0) => {IH} i Hi. exists (S i) ; split. simpl ; apply (proj1 (Nat.succ_lt_mono _ _)), Hi => /=. apply Hi. case: H => i [Hi [Ht Ht']]. apply Rle_lt_or_eq_dec in Ht ; case: Ht => Ht. rewrite (Hval i Hi x). apply Rle_trans with (2 := RmaxLess2 _ _). rewrite /M_ly ; case: (ly). apply Rle_refl. move => y ly' ; elim: ly' (i) y. move => i0 y ; case: i0 => //=. apply RmaxLess1. move => _; apply RmaxLess2. move => y ly' IH i0 y' ; case: i0. apply RmaxLess1. move => n ; apply Rle_trans with (1 := IH n y) ; apply RmaxLess2. split => //. rewrite -Ht ; apply Rle_trans with (2 := RmaxLess1 _ _). case: (i). apply RmaxLess1. move => n ; elim: n (h) (h') (l). move => h0 h'0 l0 ; apply Rle_trans with (2 := RmaxLess2 _ _), RmaxLess1. move => n IH h0 h'0 l0. case: l0. apply Rle_trans with (2 := RmaxLess2 _ _), RmaxLess2. move => h''0 l0 ; apply Rle_trans with (1 := IH h''0 h0 l0), RmaxLess2. rewrite Hx' /b -Hlast. apply Rle_trans with (2 := RmaxLess1 _ _). elim: (l) (h') (h) => [| h''0 l0 IH] h'0 h0. apply Rle_trans with (2 := RmaxLess2 _ _), RmaxLess1. apply Rle_trans with (1 := IH h0 h''0), RmaxLess2. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)