proposition: Lemma StepFun_P7 : forall (a b r1 r2 r3:R) (f:R -> R) (l lf:list R), a <= b -> adapted_couple f a b (cons r1 (cons r2 l)) (cons r3 lf) -> adapted_couple f r2 b (cons r2 l) lf.
proof: Proof. unfold adapted_couple; intros; decompose [and] H0; clear H0; assert (H5 : Rmax a b = b). { unfold Rmax; decide (Rle_dec a b) with H; reflexivity. } assert (H7 : r2 <= b). { rewrite H5 in H2; rewrite <- H2; apply RList_P7; [ assumption | simpl; right; left; reflexivity ]. } repeat split. - apply RList_P4 with r1; assumption. - rewrite H5 in H2; unfold Rmin; decide (Rle_dec r2 b) with H7; reflexivity. - unfold Rmax; decide (Rle_dec r2 b) with H7. rewrite H5 in H2; rewrite <- H2; reflexivity. - simpl in H4; simpl; apply INR_eq; apply Rplus_eq_reg_l with 1; do 2 rewrite (Rplus_comm 1); do 2 rewrite <- S_INR; rewrite H4; reflexivity. - intros; unfold constant_D_eq, open_interval; intros; unfold constant_D_eq, open_interval in H6; assert (H9 : (S i < pred (length (cons r1 (cons r2 l))))%nat). + simpl; simpl in H0; apply -> Nat.succ_lt_mono; assumption. + assert (H10 := H6 _ H9); apply H10; assumption. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra