proposition: Lemma sqrt_sqr_except: forall x y:R, format x -> -1 <= round_flx1 (x / round_flx2(sqrt (round_flx3(round_flx4(x*x)+round_flx5(y*y))))) <= 1.
proof: Proof. Proof with auto with typeclass_instances. intros x y Fx. case (Rle_or_lt 0 x); intros Hx. split. apply Rle_trans with 0. auto with real. apply sqrt_sqr_pos... unfold Prec_gt_0; lia. apply sqrt_sqr_pos... unfold Prec_gt_0; lia. replace (x / round_flx2 (sqrt (round_flx3 (round_flx4 (x * x) + round_flx5 (y * y))))) with (-(((-x) / round_flx2 (sqrt (round_flx3 (round_flx4 ((-x) * (-x)) + round_flx5 (y * y))))))). rewrite round_N_opp. split. apply Ropp_le_contravar. apply sqrt_sqr_pos... unfold Prec_gt_0; lia. now apply generic_format_opp. auto with real. apply Rle_trans with (-0). apply Ropp_le_contravar. apply sqrt_sqr_pos... unfold Prec_gt_0; lia. now apply generic_format_opp. auto with real. rewrite Ropp_0; auto with real. unfold Rdiv; rewrite Ropp_mult_distr_l_reverse, Ropp_involutive. repeat apply f_equal; apply f_equal2; apply f_equal; ring. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic)