proposition: Lemma Rint_minus : forall f g a b x y, Rint f a b x -> Rint g a b y -> Rint (f - g)%F a b (x - y).
proof: Proof. intros f g a b x y [prf Hf] [prg Hg]; unfold minus_fct. apply Rint_eq_compat with (fun u => f u + (-1) * g u). intros; ring. replace (x - y) with (x+(-1)*y) by ring. pose proof RiemannInt_P10 (-1) prf prg as prfg. exists prfg. rewrite RiemannInt_P13 with _ _ _ _ _ prf prg prfg. rewrite Hf, Hg; reflexivity. Qed.
imports: Reals RiemannInt RIneq Lra R_sqr MyRfunctions