proposition: Lemma StepFun_P39 : forall (a b:R) (f:StepFun a b), RiemannInt_SF f = - RiemannInt_SF (mkStepFun (StepFun_P6 (pre f))).
proof: Proof. intros; unfold RiemannInt_SF; case (Rle_dec a b); case (Rle_dec b a); intros. - assert (H : adapted_couple f a b (subdivision f) (subdivision_val f)); [ apply StepFun_P1 | assert (H0 : adapted_couple (mkStepFun (StepFun_P6 (pre f))) b a (subdivision (mkStepFun (StepFun_P6 (pre f)))) (subdivision_val (mkStepFun (StepFun_P6 (pre f))))); [ apply StepFun_P1 | assert (H1 : a = b); [ apply Rle_antisym; assumption | rewrite (StepFun_P8 H H1); assert (H2 : b = a); [ symmetry ; apply H1 | rewrite (StepFun_P8 H0 H2); ring ] ] ] ]. - rewrite Ropp_involutive; eapply StepFun_P17; [ apply StepFun_P1 | apply StepFun_P2; set (H := StepFun_P6 (pre f)); unfold IsStepFun in H; elim H; intros; unfold is_subdivision; elim p; intros; apply p0 ]. - apply Ropp_eq_compat; eapply StepFun_P17; [ apply StepFun_P1 | apply StepFun_P2; set (H := StepFun_P6 (pre f)); unfold IsStepFun in H; elim H; intros; unfold is_subdivision; elim p; intros; apply p0 ]. - assert (H : a < b); [ auto with real | assert (H0 : b < a); [ auto with real | elim (Rlt_irrefl _ (Rlt_trans _ _ _ H H0)) ] ]. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra