proposition: Theorem round_flx_sqr_sqrt_middle: x = sqrt (IZR beta) * bpow (mag beta x - 1) -> z=x.
proof: Proof. Proof with auto with typeclass_instances. intros Hx. unfold z, y. replace (round_flx1 (x * x)) with (bpow (2*mag beta x -1)). replace (sqrt (bpow (2 * mag beta x - 1))) with x. apply round_generic... apply sym_eq, sqrt_lem_1. apply bpow_ge_0. now left. rewrite Hx at 1. rewrite Rmult_comm; rewrite Hx at 1. apply trans_eq with ((sqrt (IZR beta)*sqrt (IZR beta)) * (bpow (mag beta x-1)*bpow (mag beta x-1))). ring. rewrite <- bpow_plus, sqrt_def, <- bpow_1, <- bpow_plus. apply f_equal; ring. left; apply radix_pos. replace (x*x) with (bpow (2 * mag beta x - 1)). apply sym_eq, round_generic... apply generic_format_bpow. unfold FLX_exp; lia. apply sym_eq; rewrite Hx at 1. rewrite Rmult_comm; rewrite Hx at 1. apply trans_eq with ((sqrt (IZR beta)*sqrt (IZR beta)) * (bpow (mag beta x-1)*bpow (mag beta x-1))). ring. rewrite <- bpow_plus, sqrt_def, <- bpow_1, <- bpow_plus. apply f_equal; ring. left; apply radix_pos. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic)