proposition: Lemma TruncOpp : forall {R : ConstructiveReals} (x : CRcarrier R) (k : positive), - CRmax (CRmin x (CR_of_Q _ (Z.pos k # 1))) (CR_of_Q _ (Z.neg k # 1)) == CRmax (CRmin (-x) (CR_of_Q _ (Z.pos k # 1))) (CR_of_Q _ (Z.neg k # 1)).
proof: Proof. intros. destruct (CRltLinear R). setoid_replace (-x) with (-(1) * x). destruct (s (CR_of_Q R (Z.neg k # 1)) x 0). apply CR_of_Q_lt. reflexivity. rewrite CRmax_left, (CRmin_left (- (1) * x)). - setoid_replace (CR_of_Q R (Z.neg k # 1)) with (-(1) * CR_of_Q R (Z.pos k # 1)). rewrite CRmax_min_mult_neg. rewrite <- CRopp_mult_distr_l. rewrite CRmult_1_l. reflexivity. apply (CRplus_le_reg_l 1). rewrite CRplus_opp_r, CRplus_0_r. apply CRlt_asym, CRzero_lt_one. rewrite <- CRopp_mult_distr_l, CRmult_1_l, <- CR_of_Q_opp. apply CR_of_Q_morph. reflexivity. - rewrite <- CRopp_mult_distr_l, CRmult_1_l. rewrite <- (CRopp_involutive (CR_of_Q R (Z.pos k # 1))). apply CRopp_ge_le_contravar. rewrite <- CR_of_Q_opp. apply (CRle_trans _ (CR_of_Q R (Z.neg k # 1))). apply CR_of_Q_le. apply Qle_refl. apply CRlt_asym, c. - apply CRmin_glb. apply CRlt_asym, c. apply CR_of_Q_le. discriminate. - rewrite CRmin_left, (CRmax_left (CRmin (- (1) * x) (CR_of_Q R (Z.pos k # 1)))). setoid_replace (CR_of_Q R (Z.pos k # 1)) with (-(1) * CR_of_Q R (Z.neg k # 1)). rewrite CRmin_max_mult_neg, <- CRopp_mult_distr_l, CRmult_1_l. reflexivity. apply (CRplus_le_reg_l 1). rewrite CRplus_opp_r, CRplus_0_r. apply CRlt_asym, CRzero_lt_one. rewrite <- CRopp_mult_distr_l, CRmult_1_l, <- CR_of_Q_opp. apply CR_of_Q_morph. reflexivity. apply CRmin_glb. apply (CRle_trans _ 0). apply CR_of_Q_le. discriminate. rewrite <- CRopp_mult_distr_l, CRmult_1_l, <- CRopp_0. apply CRopp_ge_le_contravar, CRlt_asym, c. apply CR_of_Q_le. discriminate. apply (CRle_trans _ 0). apply CRlt_asym, c. apply CR_of_Q_le. discriminate. - rewrite <- CRopp_mult_distr_l, CRmult_1_l. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile