proposition: Lemma CRabs_triang : forall {R : ConstructiveReals} (x y : CRcarrier R), CRabs R (x + y) <= CRabs R x + CRabs R y.
proof: Proof. intros. rewrite <- CRabs_def. split. - apply (CRle_trans _ (CRplus R (CRabs R x) y)). + apply CRplus_le_compat_r. pose proof (CRabs_def R x (CRabs R x)) as [_ H1]. apply H1, CRle_refl. + apply CRplus_le_compat_l. pose proof (CRabs_def R y (CRabs R y)) as [_ H1]. apply H1, CRle_refl. - apply (CRle_trans _ (CRplus R (CRopp R x) (CRopp R y))). + apply CRopp_plus_distr. + apply (CRle_trans _ (CRplus R (CRabs R x) (CRopp R y))). * apply CRplus_le_compat_r. pose proof (CRabs_def R x (CRabs R x)) as [_ H1]. apply H1, CRle_refl. * apply CRplus_le_compat_l. pose proof (CRabs_def R y (CRabs R y)) as [_ H1]. apply H1, CRle_refl. Qed.
imports: QArith Qabs ConstructiveReals