proposition: Lemma CR_of_Q_abs : forall {R : ConstructiveReals} (q : Q), CRabs R (CR_of_Q R q) == CR_of_Q R (Qabs q).
proof: Proof. intros. destruct (Qlt_le_dec 0 q). - apply (CReq_trans _ (CR_of_Q R q)). + apply CRabs_right. apply CR_of_Q_le. apply Qlt_le_weak, q0. + apply CR_of_Q_morph. symmetry. apply Qabs_pos, Qlt_le_weak, q0. - apply (CReq_trans _ (CR_of_Q R (-q))). + apply (CReq_trans _ (CRabs R (CRopp R (CR_of_Q R q)))). * apply CReq_sym, CRabs_opp. * apply (CReq_trans _ (CRopp R (CR_of_Q R q))). -- apply CRabs_right. apply (CRle_trans _ (CR_of_Q R (-q))). ++ apply CR_of_Q_le. apply (Qplus_le_l _ _ q). ring_simplify. exact q0. ++ apply CR_of_Q_opp. -- apply CReq_sym, CR_of_Q_opp. + apply CR_of_Q_morph; symmetry; apply Qabs_neg, q0. Qed.
imports: QArith Qabs ConstructiveReals