proposition: Lemma C_RInt_comp_lin (f : R -> C) (u v a b : R) : C_RInt (fun y : R => (u * f (u * y + v)%R)) a b = C_RInt f (u * a + v) (u * b + v).
proof: Proof. apply injective_projections ; simpl ; rewrite -RInt_comp_lin ; apply RInt_ext => x _ ; ring. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)