proposition: Lemma Integral_eq_zero : forall a b Hab (F : PartIR) contF x, Compact Hab x -> (forall Hx, [0] [<] F x Hx) -> (forall x, Compact Hab x -> forall Hx, [0] [<=] F x Hx) -> Integral (a:=a) (b:=b) (Hab:=Hab) (F:=F) contF [=] [0] -> a [=] b.
proof: Proof. intros a b Hab F contF x H X H0 H1. apply not_ap_imp_eq; intro. apply less_irreflexive_unfolded with (x := ZeroR). apply less_wdr with (AbsIR (Integral contF)). 2: Step_final (AbsIR [0]). apply Integral_ap_zero with x (contin_imp_inc _ _ _ _ contF x H); auto. Qed.
imports: CoRN.ftc.Integral CoRN.ftc.MoreFunctions