proposition: Theorem round_flx_sqr_sqrt_exact: forall x, format x -> (beta <= 4)%Z -> round_flx2(sqrt (round_flx1(x*x))) = Rabs x.
proof: Proof. Proof with auto with typeclass_instances. intros x Fx Hradix. case (Rle_or_lt 0 x) as [H1|H1]. destruct H1. rewrite Rabs_right;[idtac|apply Rle_ge; now left]. now apply round_flx_sqr_sqrt_exact_pos. rewrite <- H, Rabs_R0, Rmult_0_l. rewrite round_0... rewrite sqrt_0. apply round_0... replace (x*x) with ((-x)*(-x)) by ring. rewrite Rabs_left1; auto with real. apply round_flx_sqr_sqrt_exact_pos; trivial. auto with real. now apply generic_format_opp. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic)