proposition: Lemma Rint_constant : forall c a b, Rint (fct_cte c) a b (c*(b-a)).
proof: Proof. intros c a b. pose proof RiemannInt_P14 a b c as pr. exists pr. apply RiemannInt_P15. Qed.
imports: Reals RiemannInt RIneq Lra R_sqr MyRfunctions