proposition: Lemma CR_of_Q_inv : forall {R : ConstructiveReals} (q : Q) (qPos : Qlt 0 q), CR_of_Q R (/q) == (/ CR_of_Q R q) (inr (CR_of_Q_pos q qPos)).
proof: Proof. intros. apply (CRmult_eq_reg_l (CR_of_Q R q)). - right. apply CR_of_Q_pos, qPos. - rewrite CRinv_r, <- CR_of_Q_mult. apply CR_of_Q_morph. field. intro abs. rewrite abs in qPos. exact (Qlt_irrefl 0 qPos). Qed.
imports: QArith Qabs Qround