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