proposition: Lemma CRnegPartAbsMin : forall {R : ConstructiveReals} (x : CRcarrier R), CRmin 0 x == (x - CRabs _ x) * (CR_of_Q _ (1#2)).
proof: Proof. intros. unfold CRmin. unfold CRminus. rewrite CRplus_0_l. apply CRmult_morph. 2: reflexivity. rewrite CRopp_0, CRplus_0_r. reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs ConstructiveRealsMorphisms