proposition: Lemma StepFun_P45 : forall (f:R -> R) (a b c:R), IsStepFun f a b -> a <= c <= b -> IsStepFun f c b.
proof: Proof. intros f; intros; assert (H0 : a <= b). { elim H; intros; apply Rle_trans with c; assumption. } elim H; clear H; intros; unfold IsStepFun in X; unfold is_subdivision in X; elim X; clear X; intros l1 [lf1 H2]; cut (forall (l1 lf1:list R) (a b c:R) (f:R -> R), adapted_couple f a b l1 lf1 -> a <= c <= b -> { l:list R & { l0:list R & adapted_couple f c b l l0 } }). { intro X; unfold IsStepFun; unfold is_subdivision; eapply X; [ apply H2 | split; assumption ]. } clear f a b c H0 H H1 H2 l1 lf1; simple induction l1. { intros; unfold adapted_couple in H; decompose [and] H; clear H; simpl in H4; discriminate. } intros r r0; elim r0. { intros X lf1 a b c f H H0; assert (H1 : a = b). { unfold adapted_couple in H; decompose [and] H; clear H; simpl in H3; simpl in H2; assert (H7 : a <= b). { elim H0; intros; apply Rle_trans with c; assumption. } replace a with (Rmin a b). { pattern b at 2; replace b with (Rmax a b). { rewrite <- H2; rewrite H3; reflexivity. } unfold Rmax; decide (Rle_dec a b) with H7; reflexivity. } unfold Rmin; decide (Rle_dec a b) with H7; reflexivity. } split with (cons r nil); split with lf1; assert (H2 : c = b). { rewrite H1 in H0; elim H0; intros; apply Rle_antisym; assumption. } rewrite <- H2 in H1; rewrite <- H1; assumption. } intros r1 r2 _ X0 lf1 a b c f H H0; induction lf1 as [| r3 lf1 Hreclf1]. { unfold adapted_couple in H; decompose [and] H; clear H; simpl in H4; discriminate. } clear Hreclf1; assert (H1 : {c <= r1} + {r1 < c}). { case (Rle_dec c r1); intro; [ left; assumption | right; auto with real ]. } elim H1; intro a0. { split with (cons c (cons r1 r2)); split with (cons r3 lf1); unfold adapted_couple in H; decompose [and] H; clear H; unfold adapted_couple; repeat split. - unfold ordered_Rlist; intros; simpl in H; induction i as [| i Hreci]. { simpl; assumption. } clear Hreci; apply (H2 (S i)); simpl; assumption. - simpl; unfold Rmin; case (Rle_dec c b) as [|[]]; [ reflexivity | elim H0; intros; assumption ]. - replace (Rmax c b) with (Rmax a b). { rewrite <- H3; reflexivity. } unfold Rmax; case (Rle_dec c b) as [|[]]; case (Rle_dec a b) as [|[]]; [ reflexivity | elim H0; intros; apply Rle_trans with c; assumption | elim H0; intros; assumption | elim H0; intros; apply Rle_trans with c; assumption ]. - simpl; simpl in H5; apply H5. - intros; simpl in H; induction i as [| i Hreci]. { unfold constant_D_eq, open_interval; intros; simpl; apply (H7 0%nat). { simpl; apply Nat.lt_0_succ. } unfold open_interval; simpl; simpl in H6; elim H6; clear H6; intros; split; try assumption; apply Rle_lt_trans with c; try assumption; replace r with a. { elim H0; intros; assumption. } simpl in H4; rewrite H4; unfold Rmin; case (Rle_dec a b) as [|[]]; [ reflexivity | elim H0; intros; apply Rle_trans with c; assumption ]. } clear Hreci; apply (H7 (S i)); simpl; assumption. } cut (adapted_couple f r1 b (cons r1 r2) lf1). { cut (r1 <= c <= b). { intros; elim (X0 _ _ _ _ _ H3 H2); intros l1' [lf1' H4]; split with l1'; split with lf1'; assumption. } split; [ left; assumption | elim H0; intros; assumption ]. } eapply StepFun_P7; [ elim H0; intros; apply Rle_trans with c; [ apply H2 | apply H3 ] | apply H ]. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra