proposition: Lemma StepFun_P11 : forall (a b r r1 r3 s1 s2 r4:R) (r2 lf1 s3 lf2:list R) (f:R -> R), a < b -> adapted_couple f a b (cons r (cons r1 r2)) (cons r3 lf1) -> adapted_couple_opt f a b (cons s1 (cons s2 s3)) (cons r4 lf2) -> r1 <= s2.
proof: Proof. intros; unfold adapted_couple_opt in H1; elim H1; clear H1; intros; unfold adapted_couple in H0, H1; decompose [and] H0; decompose [and] H1; clear H0 H1; assert (H12 : r = s1). { simpl in H10; simpl in H5; congruence. } assert (H14 := H3 0%nat (Nat.lt_0_succ _)); simpl in H14; elim H14; intro. 2:{ rewrite <- H0; rewrite H12; apply (H7 0%nat); simpl; apply Nat.lt_0_succ. } assert (H15 := H7 0%nat (Nat.lt_0_succ _)); simpl in H15; elim H15; intro. 2:{ elim H2; clear H2; intros; assert (H17 := H16 0%nat); simpl in H17; elim (H17 (Nat.lt_0_succ _)); assumption. } rewrite <- H12 in H1; destruct (Rle_dec r1 s2) as [Hle|Hnle]; try assumption. assert (H16 : s2 < r1) by auto with real. induction s3 as [| r0 s3 Hrecs3]. { simpl in H9; rewrite H9 in H16; cut (r1 <= Rmax a b). { intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H17 H16)). } rewrite <- H4; apply RList_P7; [ assumption | simpl; right; left; reflexivity ]. } clear Hrecs3; induction lf2 as [| r5 lf2 Hreclf2]. { simpl in H11; discriminate. } clear Hreclf2; assert (H17 : r3 = r4). { set (x := (r + s2) / 2); assert (H17 := H8 0%nat (Nat.lt_0_succ _)); assert (H18 := H13 0%nat (Nat.lt_0_succ _)); unfold constant_D_eq, open_interval in H17, H18; simpl in H17; simpl in H18; rewrite <- (H17 x). 1: apply H18;rewrite <- H12. 1,2: unfold x; lra. } assert (H18 : f s2 = r3). { apply (H8 0%nat); [ simpl; apply Nat.lt_0_succ | unfold open_interval; simpl; split; assumption ]. } assert (H19 : r3 = r5). 2:{ elim H2; intros; assert (H22 := H20 0%nat); simpl in H22; assert (H23 := H22 (Nat.lt_0_succ _)); elim H23; intro; [ elim H24; rewrite <- H17; rewrite <- H19; reflexivity | elim H24; rewrite <- H17; assumption ]. } assert (H19 := H7 1%nat); simpl in H19; assert (H20 := H19 (proj1 (Nat.succ_lt_mono _ _) (Nat.lt_0_succ _))); elim H20; intro. 2:{ elim H2; clear H2; intros; assert (H23 := H22 1%nat); simpl in H23; assert (H24 := H23 (proj1 (Nat.succ_lt_mono _ _) (Nat.lt_0_succ _))); elim H24; assumption. } set (x := (s2 + Rmin r1 r0) / 2); assert (H22 := H8 0%nat); assert (H23 := H13 1%nat); simpl in H22; simpl in H23; rewrite <- (H22 (Nat.lt_0_succ _) x). 1:apply (H23 (proj1 (Nat.succ_lt_mono _ _) (Nat.lt_0_succ _)) x). 1,2:unfold open_interval; simpl; unfold x; unfold Rmin;destruct (Rle_dec r1 r0);lra. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra