proposition: Lemma XnegPartAbsMax : forall {R : ConstructiveReals} (x : CRcarrier R), CRmax 0 (-x) == (CRabs _ x - x) * (CR_of_Q _ (1#2)).
proof: Proof. intros. rewrite CRposPartAbsMax. rewrite CRabs_opp. apply CRmult_morph. rewrite CRplus_comm. reflexivity. reflexivity. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete