proposition: Lemma round_round_sqrt_beta_odd : forall (fexp1 fexp2 : Z -> Z), Valid_exp fexp1 -> Valid_exp fexp2 -> forall (choice1 choice2 : Z -> bool), (forall ex, (fexp2 ex <= fexp1 ex)%Z) -> forall x, generic_format beta fexp1 x -> round_round_eq beta fexp1 fexp2 choice1 choice2 (sqrt x).
proof: Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x Fx. destruct (Rle_or_lt x 0) as [Npx|Px]. { unfold round_round_eq. rewrite (sqrt_neg _ Npx). now rewrite round_0; [|apply valid_rnd_N]. } assert (Psx := sqrt_lt_R0 _ Px). specialize (Hexp (mag (sqrt x))). apply (neq_midpoint_beta_odd _ _ _ _ _ _ _ Psx Hexp). now apply sqrt_neq_midpoint. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core FTZ Double_rounding)