proposition: Lemma CRabs_le : forall {R : ConstructiveReals} (a b:CRcarrier R), (-b <= a /\ a <= b) -> CRabs R a <= b.
proof: Proof. intros. pose proof (CRabs_def R a b) as [H0 _]. apply H0. split. - apply H. - destruct H. rewrite <- (CRopp_involutive b). apply CRopp_ge_le_contravar. exact H. Qed.
imports: QArith Qabs ConstructiveReals