proposition: Lemma TruncPosNeg : forall {R : ConstructiveReals} (y : CRcarrier R) (k : positive), CRmax (CRmin (CRmax 0 y) (CR_of_Q R (Z.pos k # 1))) (CR_of_Q R (Z.neg k # 1)) + CRmax (CRmin (CRmin 0 y) (CR_of_Q R (Z.pos k # 1))) (CR_of_Q R (Z.neg k # 1)) == CRmax (CRmin y (CR_of_Q R (Z.pos k # 1))) (CR_of_Q R (Z.neg k # 1)).
proof: Proof. intros. rewrite (CRmax_left (CRmin (CRmax 0 y) (CR_of_Q R (Z.pos k # 1)))). rewrite (CRmin_left (CRmin 0 y)). - destruct (CRltLinear R). destruct (s (CR_of_Q R (Z.neg k # 1)) y 0). + apply CR_of_Q_lt. reflexivity. + rewrite (CRmax_left (CRmin y (CR_of_Q R (Z.pos k # 1)))). rewrite (CRmax_left (CRmin 0 y)). destruct (s 0 y (CR_of_Q R (Z.pos k # 1))). apply CR_of_Q_lt. reflexivity. rewrite CRmax_right, (CRmin_left 0 y). rewrite CRplus_0_r. reflexivity. apply CRlt_asym, c0. apply CRlt_asym, c0. rewrite (CRmin_left y), CRmin_left. unfold CRmax, CRmin. rewrite CRplus_0_l, <- CRmult_plus_distr_r. unfold CRminus. rewrite CRplus_assoc, <- (CRplus_comm (- CRabs R (y + - 0))). rewrite <- (CRplus_assoc (CRabs R (y + - 0))), CRplus_opp_r, CRplus_0_l. apply (CRmult_eq_reg_r (CR_of_Q R 2)). left. apply CR_of_Q_lt. reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. rewrite (CR_of_Q_plus R 1 1), CRmult_1_r, CRmult_plus_distr_l. rewrite CRmult_1_r. reflexivity. apply CRmax_lub. apply CR_of_Q_le. discriminate. apply CRlt_asym, c0. apply CRlt_asym, c0. apply CRmin_glb. apply CR_of_Q_le. discriminate. apply CRlt_asym, c. apply CRmin_glb. apply CRlt_asym, c. apply CR_of_Q_le. discriminate. + rewrite (CRmax_left 0 y). rewrite (CRmin_right 0 y). rewrite CRmin_left, CRplus_0_l. rewrite CRmin_left. reflexivity. apply (CRle_trans _ 0). apply CRlt_asym, c. apply CR_of_Q_le. discriminate. apply CR_of_Q_le. discriminate. apply CRlt_asym, c. apply CRlt_asym, c. - apply (CRle_trans _ 0). apply CRmin_l. apply CR_of_Q_le. discriminate. - apply CRmin_glb. apply (CRle_trans _ 0). apply CR_of_Q_le. discriminate. apply CRmax_l. apply CR_of_Q_le. discriminate. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile