proposition: Theorem round_flx_sqr_sqrt_exact_pos: forall x, 0 < x -> format x -> (radix_val beta <= 4)%Z -> round_flx2(sqrt (round_flx1(x*x))) = x.
proof: Proof. Proof with auto with typeclass_instances. intros x Hx Fx Hradix. case (Rle_or_lt x (sqrt (IZR beta) * bpow (mag beta x - 1))). intros H1; destruct H1. apply round_flx_sqr_sqrt_exact_case1... lia. apply round_flx_sqr_sqrt_middle... lia. intros H1. apply round_flx_sqr_sqrt_exact_aux... lia. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic)