proposition: Lemma Rint_sqrt_inv : forall a b, 0 < a -> 0 < b -> Rint (fun x => /(sqrt x)) a b (2 *( sqrt b - sqrt a)).
proof: Proof. intros a b Ha Hb. assert(Hneq : forall x, Rmin a b <= x <= Rmax a b -> 0 < sqrt x). intros; apply sqrt_lt_R0. apply Rlt_le_trans with (Rmin a b). apply Rmin_pos; assumption. intuition. apply Rint_eq_compat with (fun x => 2 * /(2 * sqrt x)). intros; field. auto with *. apply Rint_scalar_mult_compat_l. apply Rint_derive2. intros; apply derivable_pt_lim_sqrt. apply Rlt_le_trans with (Rmin a b). apply Rmin_pos; assumption. intuition. intros. apply continuity_pt_inv. apply continuity_pt_mult. apply continuity_pt_constant. apply continuity_pt_sqrt. apply Rle_trans with (Rmin a b). apply Rmin_ge; intuition. intuition. assert( 0 < 2 * sqrt x). apply Rmult_lt_0_compat. auto with *. auto. auto with *. Qed.
imports: Reals MyRfunctions Rintegral Lia