proposition: Lemma StepFun_P26 : forall (a b l:R) (f g:R -> R) (l1:list R), is_subdivision f a b l1 -> is_subdivision g a b l1 -> is_subdivision (fun x:R => f x + l * g x) a b l1.
proof: Proof. intros a b l f g l1 (x0,(H0,(H1,(H2,(H3,H4))))) (x,(_,(_,(_,(_,H9))))). exists (FF l1 (fun x:R => f x + l * g x)); repeat split. 1,2,3:assumption. - apply StepFun_P20; rewrite H3; auto with arith. - intros i H8 x1 H10; unfold open_interval in H10, H9, H4; rewrite (H9 _ H8 _ H10); rewrite (H4 _ H8 _ H10); assert (H11 : l1 <> nil). { red; intro H11; rewrite H11 in H8; elim (Nat.nlt_0_r _ H8). } destruct (RList_P19 _ H11) as (r,(r0,H12)); rewrite H12; unfold FF; change (pos_Rl x0 i + l * pos_Rl x i = pos_Rl (map (fun x2:R => f x2 + l * g x2) (mid_Rlist (cons r r0) r)) (S i)); rewrite RList_P12. { rewrite RList_P13. { rewrite <- H12; rewrite (H9 _ H8); try rewrite (H4 _ H8); lra. } rewrite <- H12; assumption. } rewrite RList_P14; simpl; rewrite H12 in H8; simpl in H8; apply -> Nat.succ_lt_mono; apply H8. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra