proposition: Lemma FLT_round_round_sqrt_hyp : (emin <= 0)%Z -> ((emin' <= emin - prec - 2)%Z \/ (2 * emin' <= emin - 4 * prec - 2)%Z) -> (2 * prec + 2 <= prec')%Z -> round_round_sqrt_hyp (FLT_exp emin prec) (FLT_exp emin' prec').
proof: Proof. intros Hemin Heminprec Hprec. unfold FLT_exp. unfold Prec_gt_0 in prec_gt_0_. unfold round_round_sqrt_hyp; split; [|split]; intros ex. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (2 * ex - prec) emin). lia. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (2 * ex - 1 - prec) emin). lia. - generalize (Zmax_spec (2 * ex - prec) emin). generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ex - prec) emin). lia. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ