proposition: Lemma Rint_continuous_pos_eq_0 : forall f a b, a < b -> (forall x, a <= x <= b -> continuity_pt f x) -> (forall x, a <= x <= b -> 0 <= f x) -> Rint f a b 0 -> (forall x, a <= x <= b -> f x = 0).
proof: Proof. intros f a b Hab Hcont Hpos Hint x Hx. case (Req_dec (f x) 0); intro Hcase. apply Hcase. pose proof Rint_continuous_gt_0 _ _ _ _ 0 Hab Hx Hcont Hpos Hcase Hint as pr. exact (False_ind _ (Rlt_irrefl 0 pr)). Qed.
imports: Reals RiemannInt RIneq Lra R_sqr MyRfunctions