proposition: Lemma CRabs_triang_inv2 : forall {R : ConstructiveReals} (x y : CRcarrier R), CRabs R (CRabs R x - CRabs R y) <= CRabs R (x - y).
proof: Proof. intros. apply CRabs_le. split. 2: apply CRabs_triang_inv. apply (CRplus_le_reg_r (CRabs R y)). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l. rewrite CRplus_0_r. fold (x - y). rewrite CRplus_comm, CRabs_minus_sym. apply (CRle_trans _ _ _ (CRabs_triang_inv y (y-x))). setoid_replace (y - (y - x)) with x. - apply CRle_refl. - unfold CRminus. rewrite CRopp_plus_distr, <- CRplus_assoc. rewrite CRplus_opp_r, CRplus_0_l. apply CRopp_involutive. Qed.
imports: QArith Qabs ConstructiveReals