proposition: Lemma c1_2_correct : F.toX c1_2 = Xreal (/ 2).
proof: Proof. change c1_2 with (iter_pos F.div2 1 c1); rewrite c1_n_correct. { unfold c1; rewrite F.fromZ_correct by easy; simpl; apply f_equal; lra. } unfold F.toR, c1; rewrite F.fromZ_correct by easy; simpl; rewrite Rabs_R1; lra. Qed.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float