proposition: Lemma CRabs_def2 : forall {R : ConstructiveReals} (x a:CRcarrier R), CRabs _ x <= a -> (x <= a) /\ (- a <= x).
proof: Proof. split. - exact (CRle_trans _ _ _ (CRle_abs _) H). - rewrite <- (CRopp_involutive x). apply CRopp_ge_le_contravar. rewrite <- CRabs_opp in H. exact (CRle_trans _ _ _ (CRle_abs _) H). Qed.
imports: QArith Qabs ConstructiveReals