proposition: Lemma CRabs_triang_inv : forall {R : ConstructiveReals} (x y : CRcarrier R), CRabs R x - CRabs R y <= CRabs R (x - y).
proof: Proof. intros. apply (CRplus_le_reg_r (CRabs R y)). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l. rewrite CRplus_0_r. apply (CRle_trans _ (CRabs R (x - y + y))). - setoid_replace (x - y + y) with x. + apply CRle_refl. + unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l. rewrite CRplus_0_r. reflexivity. - apply CRabs_triang. Qed.
imports: QArith Qabs ConstructiveReals