proposition: Lemma FTZ_round_round_div_hyp : (emin' + prec' <= emin - 1)%Z -> (2 * prec <= prec')%Z -> round_round_div_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').
proof: Proof. intros Hemin Hprec. unfold FTZ_exp. unfold Prec_gt_0 in prec_gt_0_. unfold Prec_gt_0 in prec_gt_0_. unfold round_round_div_hyp. split; [intro ex|split; [|split; [|split]]; intros ex ey]. - destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ex - prec) emin); lia. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (ey - prec) emin); destruct (Z.ltb_spec (ex - ey - prec) emin); destruct (Z.ltb_spec (ex - ey - prec') emin'); lia. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (ey - prec) emin); destruct (Z.ltb_spec (ex - ey + 1 - prec) emin); destruct (Z.ltb_spec (ex - ey + 1 - prec') emin'); lia. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (ey - prec) emin); destruct (Z.ltb_spec (ex - ey - prec) emin); destruct (Z.ltb_spec (ex - ey - prec') emin'); lia. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (ey - prec) emin); destruct (Z.ltb_spec (ex - ey - prec) emin); destruct (Z.ltb_spec (ex - ey - prec') emin'); lia. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ