proposition: Lemma is_RInt_const_sign (f : R -> R) (If : R) a b (le_ab : a <= b) : constant_sign (fun x => Rmin a b <= x <= Rmax a b) f -> is_RInt f a b If -> is_RInt (fun x => Rabs (f x)) a b (Rabs If).
proof: Proof. move => cst_sgn fint. case: cst_sgn => [f_pos|f_neg]. - have Habs : forall x , Rmin a b < x < Rmax a b -> f x = Rabs (f x). by move => x Hx; rewrite Rabs_pos_eq //; apply: f_pos; lra. apply: (is_RInt_ext f _ _ _ _ Habs). rewrite Rabs_pos_eq // . apply: (is_RInt_ge_0 f a b If le_ab fint). by move => x Hx; apply: f_pos; rewrite Rmin_left ?Rmax_right; lra. - have Habs : forall x , Rmin a b < x < Rmax a b -> - (f x) = Rabs (f x). by move => x Hx; rewrite Rabs_left1 //; apply: f_neg; lra. apply: (is_RInt_ext _ _ _ _ _ Habs). rewrite Rabs_left1. apply: is_RInt_opp => // . apply: (is_RInt_le_0 _ a b _ le_ab) => // . exact: fint. move => x Hx. apply: f_neg. rewrite Rmin_left ?Rmax_right; lra. Qed.
imports: Coq(Reals List Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool) Stdlib Coquelicot Xreal Interval Taylor_model Interval_compl