proposition: Lemma CRabs_opp : forall {R : ConstructiveReals} (x : CRcarrier R), CRabs R (- x) == CRabs R x.
proof: Proof. intros. split. - rewrite <- CRabs_def. split. + pose proof (CRabs_def R (CRopp R x) (CRabs R (CRopp R x))) as [_ H1]. specialize (H1 (CRle_refl (CRabs R (CRopp R x)))) as [_ H1]. apply (CRle_trans _ (CRopp R (CRopp R x))). 2: exact H1. apply (CRopp_involutive x). + pose proof (CRabs_def R (CRopp R x) (CRabs R (CRopp R x))) as [_ H1]. apply H1, CRle_refl. - rewrite <- CRabs_def. split. + pose proof (CRabs_def R x (CRabs R x)) as [_ H1]. apply H1, CRle_refl. + apply (CRle_trans _ x). * apply CRopp_involutive. * pose proof (CRabs_def R x (CRabs R x)) as [_ H1]. apply H1, CRle_refl. Qed.
imports: QArith Qabs ConstructiveReals