proposition: Lemma Rint_pow_pos : forall n a b, Rint (fun y : R => INR n * y ^ (pred n)) a b ((b ^ n - a ^ n)).
proof: Proof. intros n a b. destruct n. replace (b ^ 0 - a ^ 0) with (0 * (b - a)) by ring. apply Rint_eq_compat with (fct_cte 0). unfold fct_cte; auto with *. apply Rint_constant. apply Rint_derive2 with (f := fun x => x ^ (S n)); intros. apply derivable_pt_lim_pow_pos; lia. apply continuity_pt_mult. apply continuity_pt_const; intros u v ; reflexivity. induction n. apply continuity_pt_const; intros u v ; reflexivity. simpl. apply continuity_pt_mult. auto with Rcont. auto with Rcont. Qed.
imports: Reals MyRfunctions Rintegral Lia