proposition: Lemma CRabs_right : forall {R : ConstructiveReals} (x : CRcarrier R), 0 <= x -> CRabs R x == x.
proof: Proof. intros. split. - pose proof (CRabs_def R x (CRabs R x)) as [_ H1]. apply H1, CRle_refl. - rewrite <- CRabs_def. split. + apply CRle_refl. + apply (CRle_trans _ 0). 2: exact H. apply (CRle_trans _ (CRopp R 0)). * intro abs. apply CRopp_lt_cancel in abs. contradiction. * apply (CRplus_le_reg_l 0). apply (CRle_trans _ 0). -- apply CRplus_opp_r. -- apply CRplus_0_r. Qed.
imports: QArith Qabs ConstructiveReals