proposition: Lemma FLX_round_round_sqrt_hyp : (2 * prec + 2 <= prec')%Z -> round_round_sqrt_hyp (FLX_exp prec) (FLX_exp prec').
proof: Proof. intros Hprec. unfold FLX_exp. unfold Prec_gt_0 in prec_gt_0_. unfold round_round_sqrt_hyp; split; [|split]; intro ex; lia. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ