proposition: Lemma err_sqrt_aux: forall x, bpow (Zceil ((IZR (emin+prec-1))/2)) < round_flt (sqrt x) -> bpow (emin+prec-1) < x.
proof: Proof. Proof with auto with typeclass_instances. intros x H. case (Rle_or_lt x (bpow (emin + prec - 1))); intros H1;[idtac|easy]. contradict H. apply Rle_not_lt. apply round_le_generic... apply generic_format_bpow. unfold FLT_exp. rewrite Z.max_l. lia. cut (emin + prec-1 <= Zceil (IZR (emin + prec - 1) / 2))%Z. lia. rewrite <- (Zceil_IZR (emin+prec-1)) at 1. apply Zceil_le. apply Rmult_le_reg_l with 2%R. intuition. apply Rplus_le_reg_l with (-IZR (emin+prec-1)). apply Rle_trans with (IZR (emin + prec - 1));[right; ring|idtac]. apply Rle_trans with 0%R;[idtac|right;simpl;field]. apply IZR_le. lia. apply Rle_trans with (sqrt (bpow (emin + prec - 1))). now apply sqrt_le_1_alt. apply Rle_trans with (sqrt (bpow (2*Zceil (IZR (emin + prec - 1) / 2)))). apply sqrt_le_1_alt. apply bpow_le. apply le_IZR. rewrite mult_IZR. apply Rle_trans with ( 2 * ((IZR (emin + prec - 1) / 2))). right; field. apply Rmult_le_compat_l. intuition. apply Zceil_ub. right; apply sqrt_lem_1. apply bpow_ge_0. apply bpow_ge_0. rewrite <- bpow_plus. apply f_equal. ring. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)