proposition: Lemma CReal_abs_def2 : forall x a:CReal, CReal_abs x <= a -> (x <= a) /\ (- a <= x).
proof: Proof. split. - exact (CReal_le_trans _ _ _ (CReal_le_abs _) H). - rewrite <- (CReal_opp_involutive x). apply CReal_opp_ge_le_contravar. rewrite <- CReal_abs_opp in H. exact (CReal_le_trans _ _ _ (CReal_le_abs _) H). Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra