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