proposition: Lemma FTZ_round_round_sqrt_hyp : (2 * (emin' + prec') <= emin + prec <= 1)%Z -> (2 * prec + 2 <= prec')%Z -> round_round_sqrt_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').
proof: Proof. intros Hemin Hprec. unfold FTZ_exp. unfold Prec_gt_0 in *. unfold round_round_sqrt_hyp; split; [|split]; intros ex. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (2 * ex - prec) emin); lia. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (2 * ex - 1 - prec) emin); lia. - intro H. destruct (Zle_or_lt emin (2 * ex - prec)) as [H'|H']. + destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ex - prec) emin); lia. + exfalso. rewrite (Zlt_bool_true _ _ H') in H. lia. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ