proposition: Lemma Rint_abs_le_int : forall f a b x, a <= b -> Rint f a b x -> {y : R & (Rint (fun u => Rabs (f u)) a b y) & (Rabs x <= y)}.
proof: Proof. intros f a b x Hab [prf Hf]. pose proof RiemannInt_P16 prf as prabs. exists (RiemannInt prabs). exists prabs. reflexivity. rewrite <- Hf. apply RiemannInt_P17. apply Hab. Qed.
imports: Reals RiemannInt RIneq Lra R_sqr MyRfunctions