proposition: Lemma nullary_bnd_correct : forall prec o, contains (I.convert (nullary_bnd prec o)) (Xreal (nullary_real o)).
proof: Proof. intros prec [n|r n|]. - apply I.fromZ_correct. - simpl. replace (bpow' r n) with (powerRZ (IZR r) n). apply J.power_int_correct. apply I.fromZ_correct. destruct n as [|n|n] ; simpl ; try rewrite Zpower_pos_powerRZ ; easy. - apply I.pi_correct. Qed.
imports: Coq(Reals List) Xreal Basic Interval