proposition: Lemma pi_correct : forall prec, contains (convert (pi prec)) (Xreal PI).
proof: Proof. intros prec. unfold pi. replace (Xreal PI) with (Xmul (Xreal (PI/4)) (Xreal (Raux.bpow radix2 2))). change (Xreal (Raux.bpow _ _)) with (Xreal 2 * Xreal 2)%XR. rewrite <-Xmul_assoc. do 2 apply mul2_correct. apply T.pi4_correct. change (Raux.bpow _ _) with 4%R. simpl. apply f_equal. field. Qed.
imports: Coq(Reals Psatz) Xreal Basic Sig Interval Float Transcend