proposition: Lemma CReal_abs_triang : forall x y : CReal, CReal_abs (x + y) <= CReal_abs x + CReal_abs y.
proof: Proof. intros. apply CReal_abs_le. split. - setoid_replace (x + y) with (-(-x - y)). 2: ring. apply CReal_opp_ge_le_contravar. apply CReal_plus_le_compat; rewrite <- CReal_abs_opp; apply CReal_le_abs. - apply CReal_plus_le_compat; apply CReal_le_abs. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra