proposition: Lemma StepFun_P8 : forall (f:R -> R) (l1 lf1:list R) (a b:R), adapted_couple f a b l1 lf1 -> a = b -> Int_SF lf1 l1 = 0.
proof: Proof. simple induction l1. { intros; induction lf1 as [| r lf1 Hreclf1]; reflexivity. } intros r r0. induction r0 as [ | r1 r2 H0]. - intros; induction lf1 as [| r1 lf1 Hreclf1]. + reflexivity. + unfold adapted_couple in H0; decompose [and] H0; clear H0; simpl in H5; discriminate. - intros H. induction lf1 as [| r3 lf1 Hreclf1]; intros a b H1 H2. + reflexivity. + simpl; cut (r = r1). * intros H3. rewrite H3; rewrite (H lf1 r b). -- ring. -- rewrite H3; apply StepFun_P7 with a r r3; [ right; assumption | assumption ]. -- clear H H0 Hreclf1; unfold adapted_couple in H1. decompose [and] H1. intros; simpl in H4; rewrite H4; unfold Rmin; case (Rle_dec a b); intro; [ assumption | reflexivity ]. * unfold adapted_couple in H1; decompose [and] H1; intros; apply Rle_antisym. -- apply (H3 0%nat); simpl; apply Nat.lt_0_succ. -- simpl in H5; rewrite H2 in H5; rewrite H5; replace (Rmin b b) with (Rmax a b); [ rewrite <- H4; apply RList_P7; [ assumption | simpl; right; left; reflexivity ] | unfold Rmin, Rmax; case (Rle_dec b b); case (Rle_dec a b); intros; try assumption || reflexivity ]. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra