proposition: Lemma StepFun_P36 : forall (a b:R) (f g:StepFun a b) (l:list R), a <= b -> is_subdivision f a b l -> is_subdivision g a b l -> (forall x:R, a < x < b -> f x <= g x) -> RiemannInt_SF f <= RiemannInt_SF g.
proof: Proof. intros; unfold RiemannInt_SF; decide (Rle_dec a b) with H. replace (Int_SF (subdivision_val f) (subdivision f)) with (Int_SF (FF l f) l). - replace (Int_SF (subdivision_val g) (subdivision g)) with (Int_SF (FF l g) l). + unfold is_subdivision in X; elim X; clear X; intros; unfold adapted_couple in p; decompose [and] p; clear p; assert (H5 : Rmin a b = a); [ unfold Rmin; decide (Rle_dec a b) with H; reflexivity | assert (H7 : Rmax a b = b); [ unfold Rmax; decide (Rle_dec a b) with H; reflexivity | rewrite H5 in H3; rewrite H7 in H2; eapply StepFun_P35 with a b; assumption ] ]. + apply StepFun_P17 with (fe g) a b; [ apply StepFun_P21; assumption | apply StepFun_P1 ]. - apply StepFun_P17 with (fe f) a b; [ apply StepFun_P21; assumption | apply StepFun_P1 ]. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra