proposition: Lemma minusPosNegPart : forall {R : ConstructiveReals} (x : CRcarrier R), x == (CRmax 0 x) - (CRmax 0 (-x)).
proof: Proof. split. - apply (CRplus_le_reg_l (CRmax 0 (-x))). rewrite CRplus_comm. unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. apply CRmax_lub. apply (CRplus_le_reg_l (-x)). rewrite CRplus_0_r, CRplus_comm, CRplus_assoc, CRplus_opp_r, CRplus_0_r. apply CRmax_r. apply (CRplus_le_reg_l (-x)). rewrite CRplus_opp_l, CRplus_comm, CRplus_assoc, CRplus_opp_r, CRplus_0_r. apply CRmax_l. - apply (CRplus_le_reg_l (CRmax 0 (-x) - x)). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. rewrite CRplus_comm, CRplus_assoc, <- (CRplus_assoc (-CRmax 0 (-x))). rewrite CRplus_opp_l, CRplus_0_l. apply CRmax_lub. apply (CRplus_le_reg_l x). rewrite CRplus_0_r, CRplus_comm, CRplus_assoc, CRplus_opp_l, CRplus_0_r. apply CRmax_r. rewrite <- (CRplus_0_l (-x)). rewrite <- CRplus_assoc. apply CRplus_le_compat_r. rewrite CRplus_0_r. apply CRmax_l. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase