proposition: Lemma Rint_continuous_gt_0 : forall f a b u X, a < b -> a <= u <= b -> (forall x, a <= x <= b -> continuity_pt f x) -> (forall x, a <= x <= b -> 0 <= f x) -> f u <> 0 -> Rint f a b X -> 0 < X.
proof: Proof. intros f a b u X Hab Haub Hcont Hpos Hu HX. destruct (continuous_neq_0 f u (Hcont u Haub) Hu) as [eps Heps]. assert(exists c, exists d, a <= c <= b /\ a <= d <= b /\ c < d /\ forall x, c <= x <= d -> 0 < f x). exists (Rmax a (u -eps/2)). exists (Rmin b (u+ eps/2)). assert(Heps2 : 0 < eps/2) . apply Rlt_mult_inv_pos. apply cond_pos. auto with *. repeat split. apply RmaxLess1. apply Rmax_le. left; apply Hab. apply Rle_trans with u; [lra | intuition]. apply Rmin_ge. left; apply Hab. apply Rle_trans with u; [intuition | lra]. apply Rmin_l. case(Rle_lt_or_eq_dec a u(proj1 Haub)); intro Hau. apply Rlt_le_trans with u. apply Rmax_lt; [intuition | lra]. apply Rmin_ge; [intuition | lra]. subst. apply Rle_lt_trans with u. apply Rmax_le; lra. apply Rmin_2; lra. intros x Hx. rewrite <- Rabs_pos_eq. apply Rabs_pos_lt. replace x with (u+ (x-u)) by ring. apply (Heps (x-u)). assert( u - eps < x < u + eps) as [ Hu1 Hu2]. split. apply Rlt_le_trans with (Rmax a (u - eps/2)). apply Rlt_le_trans with (u-eps/2). lra. apply RmaxLess2. apply Hx. apply Rle_lt_trans with (Rmin b (u + eps/2)). apply Hx. apply Rle_lt_trans with (u + eps/2). apply Rmin_r. lra. apply Rabs_def1; lra. apply Hpos. split. eapply Rle_trans. apply RmaxLess1. apply (proj1 Hx). eapply Rle_trans. apply (proj2 Hx). apply Rmin_l. destruct H as [c [d [ Hacb [Hadb [Hcd Hstp]]]]]. destruct (Rint_subinterval _ _ _ _ _ Hacb HX) as [Y HY HZ']. assert(c <= d<=b) as Hcdb by intuition. destruct (Rint_subinterval _ _ _ _ _ Hcdb HZ') as [T HV HT']. destruct (continuity_ab_min f c d) as [m Hm]. apply Hcdb. intros x Hcxd. apply Hcont. split; eapply Rle_trans; [apply Hacb | apply Hcxd | apply Hcxd | apply Hadb]. apply Rlt_le_trans with ((f m) * (d - c)). apply Rmult_lt_0_compat; [apply Hstp; apply Hm | lra]. apply Rle_trans with T. apply Rint_le_compat with (fct_cte (f m)) f c d. apply Hcdb. intros; apply Hm; split; apply Rlt_le; apply H. apply Rint_constant. apply HV. apply Rle_trans with (X - Y). assert(Hcbpos : forall x : R, c <= x <= b -> 0 <= f x). intros x [H1 H2]; apply Hpos; split;[apply Rle_trans with c| ]; intuition. pose proof (Rint_pos _ _ _ _ (proj2 Hacb) Hcbpos HZ') as H. assert(0 <= X - Y - T). assert(Hdbpos : forall x : R, d <= x <= b -> 0 <= f x). intros x [H1 H2]; apply Hpos; split;[apply Rle_trans with d| ]; intuition. apply (Rint_pos _ _ _ _ (proj2 Hadb) Hdbpos HT'). lra. assert(Hacpos : forall x : R, a <= x <= c -> 0 <= f x). intros x [H1 H2]; apply Hpos; split; [ | apply Rle_trans with c]; intuition. pose proof (Rint_pos _ _ _ _ (proj1 Hacb) Hacpos HY) as H. assert(0 <= X - Y - T). assert(Hdbpos : forall x : R, d <= x <= b -> 0 <= f x). intros x [H1 H2]; apply Hpos; split;[apply Rle_trans with d| ]; intuition. apply (Rint_pos _ _ _ _ (proj2 Hadb) Hdbpos HT'). lra. Qed.
imports: Reals RiemannInt RIneq Lra R_sqr MyRfunctions