proposition: Lemma StepFun_P18 : forall a b c:R, RiemannInt_SF (mkStepFun (StepFun_P4 a b c)) = c * (b - a).
proof: Proof. intros; unfold RiemannInt_SF; case (Rle_dec a b); intro. - replace (Int_SF (subdivision_val (mkStepFun (StepFun_P4 a b c))) (subdivision (mkStepFun (StepFun_P4 a b c)))) with (Int_SF (cons c nil) (cons a (cons b nil))); [ simpl; ring | apply StepFun_P17 with (fct_cte c) a b; [ apply StepFun_P3; assumption | apply (StepFun_P1 (mkStepFun (StepFun_P4 a b c))) ] ]. - replace (Int_SF (subdivision_val (mkStepFun (StepFun_P4 a b c))) (subdivision (mkStepFun (StepFun_P4 a b c)))) with (Int_SF (cons c nil) (cons b (cons a nil))); [ simpl; ring | apply StepFun_P17 with (fct_cte c) a b; [ apply StepFun_P2; apply StepFun_P3; auto with real | apply (StepFun_P1 (mkStepFun (StepFun_P4 a b c))) ] ]. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra