proposition: Lemma StepFun_P44 : forall (f:R -> R) (a b c:R), IsStepFun f a b -> a <= c <= b -> IsStepFun f a c.
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 a c 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; 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 r (cons c nil)); split with (cons r3 nil); unfold adapted_couple in H; decompose [and] H; clear H; assert (H6 : r = a). { simpl in H4; rewrite H4; unfold Rmin; case (Rle_dec a b) as [|[]]; [ reflexivity | elim H0; intros; apply Rle_trans with c; assumption ]. } elim H0; clear H0; intros; unfold adapted_couple; repeat split. { rewrite H6; unfold ordered_Rlist; intros; simpl in H8; inversion H8; [ simpl; assumption | elim (Nat.nle_succ_0 _ H10) ]. } { simpl; unfold Rmin; decide (Rle_dec a c) with H; assumption. } { simpl; unfold Rmax; decide (Rle_dec a c) with H; reflexivity. } unfold constant_D_eq, open_interval; intros; simpl in H8; inversion H8. { simpl; assert (H10 := H7 0%nat); assert (H12 : (0 < pred (length (cons r (cons r1 r2))))%nat). { simpl; apply Nat.lt_0_succ. } apply (H10 H12); unfold open_interval; simpl; rewrite H11 in H9; simpl in H9; elim H9; clear H9; intros; split; try assumption. apply Rlt_le_trans with c; assumption. } elim (Nat.nle_succ_0 _ H11). } 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 (cons r l1'); split with (cons r3 lf1'); unfold adapted_couple in H, H4; decompose [and] H; decompose [and] H4; clear H H4 X0; assert (H14 : a <= b). { elim H0; intros; apply Rle_trans with c; assumption. } assert (H16 : r = a). { simpl in H7; rewrite H7; unfold Rmin; decide (Rle_dec a b) with H14; reflexivity. } induction l1' as [| r4 l1' Hrecl1']. { simpl in H13; discriminate. } clear Hrecl1'; unfold adapted_couple; repeat split. { unfold ordered_Rlist; intros; simpl in H; induction i as [| i Hreci]. { simpl; replace r4 with r1. { apply (H5 0%nat). simpl; apply Nat.lt_0_succ. } simpl in H12; rewrite H12; unfold Rmin; case (Rle_dec r1 c) as [|[]]; [ reflexivity | left; assumption ]. } apply (H9 i); simpl; apply Nat.succ_lt_mono; assumption. } { simpl; unfold Rmin; case (Rle_dec a c) as [|[]]; [ assumption | elim H0; intros; assumption ]. } { replace (Rmax a c) with (Rmax r1 c). { rewrite <- H11; reflexivity. } unfold Rmax; case (Rle_dec a c) as [|[]]; case (Rle_dec r1 c) as [|[]]; [ reflexivity | left; assumption | elim H0; intros; assumption | left; assumption ]. } { simpl; simpl in H13; rewrite H13; reflexivity. } intros; simpl in H; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. { simpl; assert (H17 := H10 0%nat); assert (H18 : (0 < pred (length (cons r (cons r1 r2))))%nat). { simpl; apply Nat.lt_0_succ. } apply (H17 H18); unfold open_interval; simpl; simpl in H4; elim H4; clear H4; intros; split; try assumption; replace r1 with r4. { assumption. } simpl in H12; rewrite H12; unfold Rmin; case (Rle_dec r1 c) as [|[]]; [ reflexivity | left; assumption ]. } clear Hreci; simpl; apply H15. { simpl; apply Nat.succ_lt_mono; assumption. } unfold open_interval; apply H4. } 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