proposition: Theorem pi_correct : forall prec, contains (convert (pi prec)) (Xreal PI).
proof: Proof. intros prec. cbv -[IZR PI Rle Rdiv]. interval with (i_prec 60). Qed.
imports: Coq(Reals Psatz PrimInt63 Uint63 Sint63 PArray Floats) Flocq(Core PrimFloat BinarySingleNaN) Missing.Flocq Xreal Basic Sig Interval Float Float_full Specific_bigint Specific_ops Primitive_ops Lang_expr Lang_tac Interval_helper