proposition: Lemma StepFun_P42 : forall (l1 l2:list R) (f:R -> R), pos_Rl l1 (pred (length l1)) = pos_Rl l2 0 -> Int_SF (FF (app l1 l2) f) (app l1 l2) = Int_SF (FF l1 f) l1 + Int_SF (FF l2 f) l2.
proof: Proof. intros l1 l2 f; induction l1 as [| r l1 IHl1]; intros H; [ simpl; ring | destruct l1 as [| r0 r1]; [ simpl in H; simpl; destruct l2 as [| r0 r1]; [ simpl; ring | simpl; simpl in H; rewrite H; ring ] | simpl; rewrite Rplus_assoc; apply Rplus_eq_compat_l; apply IHl1; rewrite <- H; reflexivity ] ]. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra