proposition: Lemma CReal_abs_triang_inv2 : forall x y : CReal, CReal_abs (CReal_abs x - CReal_abs y) <= CReal_abs (x - y).
proof: Proof. intros. apply CReal_abs_le. split. 2: apply CReal_abs_triang_inv. apply (CReal_plus_le_reg_r (CReal_abs y)). ring_simplify. rewrite CReal_plus_comm, CReal_abs_minus_sym. apply (CReal_le_trans _ _ _ (CReal_abs_triang_inv y (y-x))). setoid_replace (y - (y - x)) with x. 2: ring. apply CRealLe_refl. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra