proposition: Lemma StepFun_P21 : forall (a b:R) (f:R -> R) (l:list R), is_subdivision f a b l -> adapted_couple f a b l (FF l f).
proof: Proof. intros * (x & H & H1 & H0 & H2 & H4). repeat split; try assumption. - apply StepFun_P20; rewrite H2; apply Nat.lt_0_succ. - intros; assert (H5 := H4 _ H3); unfold constant_D_eq, open_interval in H5; unfold constant_D_eq, open_interval; intros; induction l as [| r l Hrecl]. + discriminate. + unfold FF; rewrite RList_P12. * simpl; change (f x0 = f (pos_Rl (mid_Rlist (cons r l) r) (S i))); rewrite RList_P13; try assumption; rewrite (H5 x0 H6); rewrite H5. -- reflexivity. -- lra. * rewrite RList_P14; simpl in H3; apply H3. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra