proposition: Lemma StepFun_P31 : forall (a b:R) (f:R -> R) (l lf:list R), adapted_couple f a b l lf -> adapted_couple (fun x:R => Rabs (f x)) a b l (map Rabs lf).
proof: Proof. unfold adapted_couple; intros; decompose [and] H; clear H; repeat split; try assumption. - symmetry ; rewrite H3; rewrite RList_P18; reflexivity. - intros; unfold constant_D_eq, open_interval; unfold constant_D_eq, open_interval in H5; intros; rewrite (H5 _ H _ H4); rewrite RList_P12; [ reflexivity | rewrite H3 in H; simpl in H; apply H ]. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra