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