proposition: Lemma TrapezeIncluded : forall {R : ConstructiveReals} (a b c d eta mu x : CRcarrier R) (etaPos : 0 < eta) (muPos : 0 < mu), a - eta == c - mu -> b + eta == d + mu -> eta <= mu -> CSUCUnitTrapeze c d mu muPos x <= CSUCUnitTrapeze a b eta etaPos x.
proof: Proof. intros. assert (CRinv R mu (inr muPos) <= CRinv R eta (inr etaPos)) as invLe. { apply (CRmult_le_reg_l mu _ _ muPos). rewrite CRinv_r. apply (CRmult_le_reg_r eta _ _ etaPos). rewrite CRmult_1_l, CRmult_assoc, CRinv_l, CRmult_1_r. exact H1. } apply CRplus_le_compat. - unfold UCUnitHeaviside. rewrite (CRinv_morph (a - (a-eta)) eta _ (inr etaPos)). rewrite (CRinv_morph (c - (c-mu)) mu _ (inr muPos)). apply CRmax_lub. apply CRmax_l. rewrite <- H. destruct (CRltLinear R). destruct (s (a-eta) x a). + apply (CRplus_lt_reg_r eta). unfold CRminus. rewrite CRplus_assoc. apply CRplus_lt_compat_l. rewrite CRplus_opp_l. exact etaPos. + apply (CRle_trans _ (CRmin 1 ((x - (a - eta)) * CRinv R eta (inr etaPos)))). 2: apply CRmax_r. apply CRmin_glb. apply CRmin_l. apply (CRle_trans _ ((x - (a - eta)) * CRinv R mu (inr muPos))). apply CRmin_r. apply CRmult_le_compat_l. rewrite <- (CRplus_opp_r (a-eta)). apply CRplus_le_compat_r, CRlt_asym, c0. exact invLe. + rewrite CRmin_right. rewrite CRmin_right. apply (CRmult_le_reg_r mu _ _ muPos). rewrite CRmult_assoc, CRinv_l, CRmult_1_r. apply (CRle_trans _ (eta * CRmax 0 ((x - (a - eta)) * CRinv R eta (inr etaPos)))). rewrite <- CRmax_mult. rewrite CRmult_0_r, CRmult_comm. rewrite CRmult_assoc, CRinv_l, CRmult_1_r. apply CRmax_r. apply CRlt_asym, etaPos. rewrite CRmult_comm. apply CRmult_le_compat_l. apply CRmax_l. exact H1. apply (CRmult_le_reg_r eta _ _ etaPos). rewrite CRmult_1_l, CRmult_assoc, CRinv_l, CRmult_1_r. apply (CRplus_le_reg_l a). unfold CRminus. rewrite CRopp_plus_distr, CRopp_involutive, <- CRplus_assoc, <- CRplus_assoc. apply CRplus_le_compat_r. rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. apply CRlt_asym, c0. apply (CRmult_le_reg_r mu _ _ muPos). rewrite CRmult_1_l, CRmult_assoc, CRinv_l, CRmult_1_r. apply (CRle_trans _ eta). apply (CRplus_le_reg_l a). unfold CRminus. rewrite CRopp_plus_distr, CRopp_involutive, <- CRplus_assoc, <- CRplus_assoc. apply CRplus_le_compat_r. rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. apply CRlt_asym, c0. exact H1. + unfold CRminus. rewrite CRopp_plus_distr, CRopp_involutive, <- CRplus_assoc. rewrite CRplus_opp_r, CRplus_0_l. reflexivity. + unfold CRminus. rewrite CRopp_plus_distr, CRopp_involutive, <- CRplus_assoc. rewrite CRplus_opp_r, CRplus_0_l. reflexivity. - apply CRopp_ge_le_contravar. unfold UCUnitHeaviside. rewrite (CRinv_morph (b + eta - b) eta _ (inr etaPos)). rewrite (CRinv_morph (d + mu - d) mu _ (inr muPos)). apply CRmax_lub. apply CRmax_l. destruct (CRltLinear R). destruct (s b x (b+eta)). + apply (CRplus_lt_reg_r 0). rewrite CRplus_assoc. apply CRplus_lt_compat_l. rewrite CRplus_0_r. exact etaPos. + apply (CRle_trans _ (CRmin 1 ((x - d) * CRinv R mu (inr muPos)))). 2: apply CRmax_r. apply CRmin_glb. apply CRmin_l. apply (CRmult_le_reg_r mu _ _ muPos). rewrite CRmult_assoc, CRinv_l, CRmult_1_r, CRmult_comm. rewrite <- (CRplus_0_r 1). setoid_replace ((x - b) * CRinv R eta (inr etaPos)) with (1 + (x - (b+eta)) * CRinv R eta (inr etaPos)). rewrite <- CRmin_plus, CRmult_plus_distr_l, CRmult_1_r. apply (CRplus_le_reg_l (-mu)). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. apply (CRle_trans _ (x - (b + eta))). assert (0 == CRinv R eta (inr etaPos) * 0). symmetry. apply CRmult_0_r. rewrite (CRmult_comm (x - (b + eta))). rewrite (CRmin_morph R 0 (CRinv R eta (inr etaPos) * 0) H2 _ _ (CReq_refl _)). rewrite CRmin_mult. apply (CRle_trans _ (CRmin 0 (x - (b + eta)))). 2: apply CRmin_r. rewrite <- CRopp_involutive, <- (CRopp_involutive (CRmin 0 (x - (b + eta)))). apply CRopp_ge_le_contravar. rewrite CRopp_involutive, CRopp_mult_distr_r, CRopp_mult_distr_r. rewrite <- (CRmult_1_l (- CRmin 0 (x - (b + eta)))), <- CRmult_assoc. rewrite <- CRmult_assoc. apply CRmult_le_compat_r. rewrite <- CRopp_0. apply CRopp_ge_le_contravar. apply (CRle_trans _ (-0)). apply CRmin_l. rewrite CRopp_0. apply CRle_refl. rewrite CRmult_1_r. apply (CRmult_le_reg_r eta _ _ etaPos). rewrite CRmult_assoc, CRinv_l, CRmult_1_r, CRmult_1_l. exact H1. apply CRlt_asym, CRinv_0_lt_compat, etaPos. unfold CRminus. rewrite H0, CRopp_plus_distr, (CRplus_comm (-mu)). rewrite CRplus_assoc. apply CRle_refl. unfold CRminus. rewrite (CRplus_comm 1), CRmult_plus_distr_r. rewrite CRmult_plus_distr_r, CRopp_plus_distr, CRmult_plus_distr_r. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite <- (CRopp_mult_distr_l eta), CRinv_r. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. reflexivity. + rewrite CRmin_right. rewrite CRmin_right. apply (CRle_trans _ ((x - d) * CRinv R mu (inr muPos))). 2: apply CRmax_r. apply (CRplus_le_reg_r (-(1))). apply (CRle_trans _ ((x - (b+eta)) * CRinv R eta (inr etaPos))). unfold CRminus. do 2 rewrite CRmult_plus_distr_r. rewrite CRopp_plus_distr, CRmult_plus_distr_r, <- (CRopp_mult_distr_l eta). rewrite CRinv_r, <- CRplus_assoc. apply CRle_refl. apply (CRle_trans _ ((x - (d+mu)) * CRinv R mu (inr muPos))). rewrite <- H0. rewrite <- CRopp_involutive. rewrite <- (CRopp_involutive ((x - (b + eta)) * CRinv R mu (inr muPos))). apply CRopp_ge_le_contravar. do 2 rewrite CRopp_mult_distr_l. apply CRmult_le_compat_l. unfold CRminus. rewrite CRopp_plus_distr, CRopp_involutive, <- (CRplus_opp_l x). apply CRplus_le_compat_l. apply CRlt_asym, c0. exact invLe. unfold CRminus. do 2 rewrite CRmult_plus_distr_r. rewrite CRopp_plus_distr, CRmult_plus_distr_r, <- (CRopp_mult_distr_l mu). rewrite CRinv_r, <- CRplus_assoc. apply CRle_refl. apply (CRmult_le_reg_r mu _ _ muPos). rewrite CRmult_assoc, CRinv_l, CRmult_1_r, CRmult_1_l. apply (CRplus_le_reg_r d). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l. rewrite CRplus_0_r, CRplus_comm, <- H0. apply CRlt_asym, c0. apply (CRmult_le_reg_r eta _ _ etaPos). rewrite CRmult_assoc, CRinv_l, CRmult_1_r, CRmult_1_l. apply (CRplus_le_reg_r b). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l. rewrite CRplus_0_r, CRplus_comm. apply CRlt_asym, c0. + unfold CRminus. rewrite CRplus_comm, <- CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_l. reflexivity. + unfold CRminus. rewrite CRplus_comm, <- CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_l. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal