proposition: Lemma Bmax_float_proof : valid_binary (S754_finite false (shift_pos (Z.to_pos prec) 1 - 1) (emax - prec)) = true.
proof: Proof. unfold valid_binary, bounded; apply andb_true_intro; split. - unfold canonical_mantissa; apply Zeq_bool_true. set (p := Z.pos (digits2_pos _)). assert (H : p = prec). { unfold p; rewrite Zpos_digits2_pos, Pos2Z.inj_sub. - rewrite shift_pos_correct, Z.mul_1_r. assert (P2pm1 : (0 <= 2 ^ prec - 1)%Z). { apply Z.lt_le_pred. apply (Zpower_gt_0 radix2). now apply Zlt_le_weak. } apply Zdigits_unique ; rewrite Z.pow_pos_fold, Z2Pos.id; [|exact prec_gt_0_]; simpl; split. + rewrite (Z.abs_eq _ P2pm1). apply Z.lt_le_pred. apply (Zpower_lt radix2). now apply Zlt_le_weak. apply Z.lt_pred_l. + rewrite Z.abs_eq by easy. apply Z.lt_pred_l. - change (Z.pos 1 < Z.pos (shift_pos (Z.to_pos prec) 1))%Z. rewrite shift_pos_correct, Z.mul_1_r, Z.pow_pos_fold. rewrite Z2Pos.id; [|exact prec_gt_0_]. now apply (Zpower_gt_1 radix2). } rewrite H. ring_simplify (prec + (emax - prec))%Z. apply fexp_emax. - apply Zle_bool_true, Z.le_refl. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative