proposition: Lemma CRabs_left : forall {R : ConstructiveReals} (x : CRcarrier R), x <= 0 -> CRabs R x == - x.
proof: Proof. intros. rewrite <- CRabs_opp. apply CRabs_right. rewrite <- CRopp_0. apply CRopp_ge_le_contravar, H. Qed.
imports: QArith Qabs ConstructiveReals