proposition: Lemma CSUCTrapezePositive : forall {R : ConstructiveReals} (a b eta x : CRcarrier R) (etaPos : 0 < eta) (leab : a <= b), prod (a-eta < x) (x < b+eta) -> 0 < (CSUCUnitTrapeze a b eta etaPos x).
proof: Proof. intros. unfold CSUCUnitTrapeze, UCUnitHeaviside. rewrite CRmax_right. rewrite (CRmin_right 1 ((x - b) * CRinv R (b + eta - b) (inr (CRlt_minus b (b + eta) (Rplus_pos_higher b eta etaPos))))). - apply (CRle_lt_trans _ (CRmax 0 ((x - b) * CRinv R (b + eta - b) (inr (CRlt_minus b (b + eta) (Rplus_pos_higher b eta etaPos)))) - CRmax 0 ((x - b) * CRinv R (b + eta - b) (inr (CRlt_minus b (b + eta) (Rplus_pos_higher b eta etaPos)))))). unfold CRminus. rewrite CRplus_opp_r. apply CRle_refl. apply CRplus_lt_compat_r. apply CRmin_lt. apply CRmax_lub_lt. apply CRzero_lt_one. 2: apply CRmax_lub_lt. + apply (CRmult_lt_reg_r (b+eta-b)). unfold CRminus. rewrite CRplus_comm, <- CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_l. exact etaPos. rewrite CRmult_assoc, CRinv_l, CRmult_1_l, CRmult_1_r. unfold CRminus. apply CRplus_lt_compat_r. apply H. + apply (CRmult_lt_reg_r (a-(a-eta))). unfold CRminus. rewrite CRopp_plus_distr, <- CRplus_assoc. rewrite CRplus_opp_r, CRplus_0_l, CRopp_involutive. exact etaPos. rewrite CRmult_assoc, CRinv_l, CRmult_0_l, CRmult_1_r. rewrite <- (CRplus_opp_r (a-eta)). apply CRplus_lt_compat_r. apply H. + apply (CRmult_lt_reg_r (b+eta-b)). unfold CRminus. rewrite CRplus_comm, <- CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_l. exact etaPos. rewrite CRmult_assoc, CRinv_l, CRmult_1_r. setoid_replace (b + eta - b) with eta. rewrite <- (CRmult_comm eta). apply (CRmult_lt_reg_r (a-(a-eta))). unfold CRminus. rewrite CRopp_plus_distr, <- CRplus_assoc. rewrite CRplus_opp_r, CRplus_0_l, CRopp_involutive. exact etaPos. rewrite CRmult_assoc, CRmult_assoc, CRinv_l, CRmult_1_r. setoid_replace (a - (a - eta)) with eta. rewrite CRmult_comm. apply CRmult_lt_compat_l. exact etaPos. apply CRplus_lt_compat_l. apply CRopp_gt_lt_contravar. apply (CRlt_le_trans _ a). apply (CRplus_lt_reg_r eta). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l. apply CRplus_lt_compat_l, etaPos. exact leab. unfold CRminus. rewrite CRopp_plus_distr, <- CRplus_assoc. rewrite CRplus_opp_r, CRplus_0_l, CRopp_involutive. reflexivity. unfold CRminus. rewrite CRplus_comm, <- CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_l. reflexivity. - apply (CRmult_le_reg_r (b+eta-b)). unfold CRminus. rewrite CRplus_comm, <- CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_l. exact etaPos. rewrite CRmult_assoc, CRinv_l, CRmult_1_l, CRmult_1_r. unfold CRminus. rewrite CRplus_comm. rewrite <- (CRplus_comm (-b)). apply CRplus_le_compat_l. apply CRlt_asym, H. - apply CRmin_glb. apply CRlt_asym, CRzero_lt_one. apply (CRmult_le_reg_r (a-(a-eta))). unfold CRminus. rewrite CRopp_plus_distr, <- CRplus_assoc. rewrite CRplus_opp_r, CRplus_0_l, CRopp_involutive. exact etaPos. rewrite CRmult_assoc, CRinv_l, CRmult_0_l, CRmult_1_r. unfold CRminus. rewrite <- (CRplus_opp_l (a-eta)), (CRplus_comm x). apply CRplus_le_compat_l. apply CRlt_asym, H. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal