proposition: Theorem binary_overflow_correct : forall m s, valid_binary (binary_overflow m s) = true.
proof: Proof. intros m s. unfold binary_overflow. case overflow_to_inf. easy. unfold valid_binary, bounded. rewrite Zle_bool_refl. rewrite Bool.andb_true_r. apply Zeq_bool_true. rewrite Zpos_digits2_pos. replace (Zdigits radix2 _) with prec. ring_simplify (prec + (emax - prec))%Z. apply fexp_emax. change 2%Z with (radix_val radix2). assert (H: (0 < radix2 ^ prec - 1)%Z). apply Zlt_succ_pred. now apply Zpower_gt_1. rewrite Z2Pos.id by exact H. apply Zle_antisym. - apply Z.lt_pred_le. apply Zdigits_gt_Zpower. rewrite Z.abs_eq by now apply Zlt_le_weak. apply Z.lt_le_pred. apply Zpower_lt. now apply Zlt_le_weak. apply Z.lt_pred_l. - apply Zdigits_le_Zpower. rewrite Z.abs_eq by now apply Zlt_le_weak. apply Z.lt_pred_l. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative