proposition: Lemma IoneValSplit : forall {IS : IntegrationSpace}, { nk : prod nat nat & I IS (XminConst (Xabs (Ione IS)) (CR_of_Q _ (1# Pos.of_nat (S (snd nk))))) (LminConstStable (CR_of_Q _ (1# Pos.of_nat (S (snd nk)))) (Xabs (Ione IS)) (invSuccRealPositive (snd nk)) (LabsStable (ElemFunc IS) (Ione IS) (IoneL IS))) < I IS (XminConst (Xabs (Ione IS)) (INR (2 + (fst nk)))) (LminIntStable (2 + (fst nk)) (Xabs (Ione IS)) (LabsStable _ _ (IoneL IS))) }.
proof: Proof. intro IS. assert (0 < I IS (Xabs (Ione IS)) (LabsStable _ _ (IoneL IS))). { apply (CRlt_le_trans _ 1). apply CRzero_lt_one. rewrite <- IoneInt. apply INonDecreasing. intros. simpl. rewrite (DomainProp _ x xF y). apply CRle_abs. } pose proof (Ilimit IS (Ione IS) (IoneL IS)) as [_ lowInt]. pose proof (CR_cv_open_above _ _ _ lowInt H) as [k kmaj]. specialize (kmaj k (Nat.le_refl k)). pose proof (Ilimit IS (Xabs (Ione IS)) (LabsStable _ _ (IoneL IS))) as [highInt _]. pose proof (CR_cv_open_below _ _ _ highInt kmaj) as [n nmaj]. exists (pair n k). apply nmaj. unfold fst. apply le_S, le_S, Nat.le_refl. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia