proposition: Lemma CRmorph_inv : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (x : CRcarrier R1) (xnz : x ≶ 0) (fxnz : CRmorph f x ≶ 0), CRmorph f ((/ x) xnz) == (/ CRmorph f x) fxnz.
proof: Proof. intros. apply (CRmult_eq_reg_r (CRmorph f x)). - destruct fxnz. + right. exact c. + left. exact c. - apply (CReq_trans _ 1). 2: apply CReq_sym, CRinv_l. apply (CReq_trans _ (CRmorph f (CRmult R1 ((/ x) xnz) x))). + apply CReq_sym, CRmorph_mult. + apply (CReq_trans _ (CRmorph f 1)). * apply CRmorph_proper. apply CRinv_l. * apply CRmorph_one. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs