proposition: Theorem round_flx_sqr_sqrt_pos: forall x, format x -> 0 < x -> (4 < radix_val beta)%Z -> ((radix_val beta=5)%Z -> (3 < prec)%Z) -> round_flx3(x/round_flx2(sqrt (round_flx1(x*x)))) <= 1.
proof: Proof. Proof with auto with typeclass_instances. intros x Fx Hx Hr1 Hr2. case (Rle_or_lt x (sqrt (IZR beta) * bpow (mag beta x - 1))); intros H1. replace (round_flx2 (sqrt (round_flx1 (x * x)))) with x. replace (x/x) with 1;[idtac|field; auto with real]. right; apply round_generic... replace 1 with (bpow 0) by reflexivity. apply generic_format_bpow. unfold FLX_exp; auto with zarith. destruct H1. rewrite round_flx_sqr_sqrt_exact_case1... lia. rewrite round_flx_sqr_sqrt_middle... lia. apply round_flx_sqr_sqrt_aux... lia. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic)