proposition: Lemma sumPosNegPart : forall {R : ConstructiveReals} (x : CRcarrier R), CRabs _ x == (CRmax 0 x) + CRmax 0 (-x).
proof: Proof. split. - apply (CRplus_le_reg_l (-CRmax 0 x)). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. apply CRmax_lub. apply (CRplus_le_reg_l (CRmax 0 x)). rewrite CRplus_0_r, <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. apply CRmax_lub. apply CRabs_pos. apply CRle_abs. apply (CRplus_le_reg_l (CRmax 0 x + x)). rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r. rewrite (CRplus_comm (CRmax 0 x)), CRplus_assoc. rewrite <- (CRplus_assoc (CRmax 0 x)), CRplus_opp_r, CRplus_0_l. apply CRmax_lub. apply (CRplus_le_reg_l (-x)). rewrite CRplus_0_r, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. rewrite <- CRabs_opp. apply CRle_abs. rewrite <- (CRplus_0_r x). rewrite CRplus_assoc. apply CRplus_le_compat_l. rewrite CRplus_0_l. apply CRabs_pos. - apply CRabs_le. split. + apply (CRplus_le_reg_l (CRmax 0 (-x) - x)). unfold CRminus. rewrite CRplus_assoc, CRplus_assoc, CRplus_opp_l. rewrite CRplus_0_r. rewrite <- CRplus_assoc, (CRplus_comm), CRopp_plus_distr. rewrite CRplus_assoc, <- (CRplus_assoc (-CRmax 0 (-x))). rewrite CRplus_opp_l, CRplus_0_l. apply (CRle_trans _ (-x)). 2: apply CRmax_r. apply (CRplus_le_reg_l (CRmax 0 x)). rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. rewrite <- (CRplus_0_l (-x)), <- CRplus_assoc. apply CRplus_le_compat_r. rewrite CRplus_0_r. apply CRmax_l. + apply (CRle_trans _ (x + CRmax 0 (-x))). rewrite <- (CRplus_0_r x). rewrite CRplus_assoc. apply CRplus_le_compat_l. rewrite CRplus_0_l. apply CRmax_l. apply CRplus_le_compat. apply CRmax_r. apply CRle_refl. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase