proposition: Lemma FindCrossingPointThreasholdDecr : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (a b eta alpha gamma : CRcarrier (RealT (ElemFunc IS))) (aPos : 0 < a) (ltab : a < b) (aeta : 0 < a - eta < a) (beta : 0 < b < b + eta) (n i j : nat), alpha <= gamma -> ((i <= 2 ^ n)%nat * ((i = (2 ^ n)%nat) + (StepApproxDiscretize f fInt a b eta aPos ltab aeta beta n (S i) < alpha)) * (alpha < StepApproxDiscretize f fInt a b eta aPos ltab aeta beta n i)) -> ((j <= 2 ^ n)%nat * ((j = (2 ^ n)%nat) + (StepApproxDiscretize f fInt a b eta aPos ltab aeta beta n (S j) < gamma)) * (gamma < StepApproxDiscretize f fInt a b eta aPos ltab aeta beta n j)) -> le j i.
proof: Proof. intros. destruct H0, H1, p, p0. destruct s, s0. - subst i. rewrite e0. apply Nat.le_refl. - subst i. exact l0. - subst j. clear l0. apply (CRlt_le_trans _ _ _ c1) in H. apply (CRlt_trans _ _ _ H) in c0. clear H c1 c. unfold StepApproxDiscretize in c0. destruct (2^n)%nat eqn:des. apply Nat.le_0_l. rewrite <- des. destruct (le_lt_dec (S (S n0)) (S n0)). exfalso. lia. destruct (le_lt_dec (S (S n0)) (S i)). + apply le_S_n in l1. pose proof (Nat.le_antisymm _ _ l l1). subst i. rewrite <- des. apply Nat.le_refl. + clear l0. apply le_S_n, le_S_n in l1. clear l. exfalso. apply (StepApproxIntegralIncr f fInt (BinarySubdiv a b n i) (BinarySubdiv a b n (S i)) (BinarySubdiv a b n n0) (BinarySubdiv a b n (S n0)) (BinarySubdivIncr a b n i (aPos, ltab)) (BinarySubdivIncr a b n n0 (aPos, ltab))). 3: exact c0. clear c0. apply CRplus_le_compat_l. do 2 rewrite CRmult_assoc. apply CRmult_le_compat_r. apply CRlt_asym, CRmult_lt_0_compat. apply CRlt_minus, ltab. apply CRpow_gt_zero, CR_of_Q_pos. reflexivity. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply Nat2Z.inj_le, l1. apply CRplus_le_compat_l. do 2 rewrite CRmult_assoc. apply CRmult_le_compat_r. apply CRlt_asym, CRmult_lt_0_compat. apply CRlt_minus, ltab. apply CRpow_gt_zero, CR_of_Q_pos. reflexivity. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply Nat2Z.inj_le, le_n_S, l1. - apply (CRlt_le_trans _ _ _ c1) in H. apply (CRlt_trans _ _ _ H) in c0. unfold StepApproxDiscretize in c0. destruct j. apply Nat.le_0_l. destruct (le_lt_dec (S (2 ^ n)) (S j)). exfalso. apply le_S_n in l1. lia. destruct (le_lt_dec (S (2 ^ n)) (S i)). apply le_S_n in l1. apply le_S_n in l2. exact (Nat.le_trans _ _ _ l1 l2). destruct (le_lt_dec (S j) i). exact l3. exfalso. apply (StepApproxIntegralIncr f fInt (BinarySubdiv a b n i) (BinarySubdiv a b n (S i)) (BinarySubdiv a b n j) (BinarySubdiv a b n (S j)) (BinarySubdivIncr a b n i (aPos, ltab)) (BinarySubdivIncr a b n j (aPos, ltab))). 3: exact c0. apply le_S_n in l3. apply CRplus_le_compat_l. do 2 rewrite CRmult_assoc. apply CRmult_le_compat_r. apply CRlt_asym, CRmult_lt_0_compat. apply CRlt_minus, ltab. apply CRpow_gt_zero, CR_of_Q_pos. reflexivity. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply Nat2Z.inj_le, l3. apply CRplus_le_compat_l. do 2 rewrite CRmult_assoc. apply CRmult_le_compat_r. apply CRlt_asym, CRmult_lt_0_compat. apply CRlt_minus, ltab. apply CRpow_gt_zero, CR_of_Q_pos. reflexivity. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply Nat2Z.inj_le, l3. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia