ROSCOQ.CartAR
Require Export CoRN.reals.faster.ARtrans.
Require Export CoRN.reals.fast.CRtrans.
Require Export CoRN.reals.faster.ARbigD.
Require Export CoRN.ftc.IntegrationRules.
Require Export Coq.Program.Tactics.
Definition R2QPrec : Qpos := QposMake 1 100.
Definition threeBy2 : bigD .
exact ((inject_Z_bigD 3) ≪ (-1)).
Defined.
Definition val : ARbigD .
exact ('threeBy2×ARpi).
Defined.
Eval vm_compute in (cast bigD Q (approximate val R2QPrec)).
Definition crNum : CR := ((('(3#2)%Q)*CRpi)).
Eval vm_compute in (approximate crNum R2QPrec).
Instance CastQAR : Cast Q ARbigD := (cast CR AR) ∘ (cast Q CR).
Eval vm_compute in (approximate (cast Q CR (3#2)%Q) R2QPrec).
Eval vm_compute in (cast bigD Q (approximate (cast Q ARbigD (3#2)%Q) R2QPrec)).
Instance Positive2Z : Cast positive Z := Zpos.