proposition: Theorem bits_of_binary_float_range: forall x, (0 <= bits_of_binary_float x < 2^(mw+ew+1))%Z.
proof: Proof. unfold bits_of_binary_float. intros [sx|sx|sx pl pl_range|sx mx ex H]. - apply join_bits_range ; now split. - apply join_bits_range. now split. clear -He_gt_0 ; lia. - apply Z.ltb_lt in pl_range. apply join_bits_range. split. easy. apply (Zpower_gt_Zdigits radix2 _ (Zpos pl)). apply Z.lt_succ_r. now rewrite <- Zdigits2_Zdigits. clear -He_gt_0 ; lia. - unfold bounded in H. apply Bool.andb_true_iff in H ; destruct H as [A B]. apply Z.leb_le in B. unfold canonical_mantissa, fexp, FLT_exp in A. apply Zeq_bool_eq in A. case Zle_bool_spec ; intros H. + apply join_bits_range. * split. clear -H ; lia. rewrite Zpos_digits2_pos in A. cut (Zpos mx < 2 ^ prec)%Z. unfold prec. rewrite Zpower_plus by (clear -Hmw ; lia). change (2^1)%Z with 2%Z. clear ; lia. apply (Zpower_gt_Zdigits radix2 _ (Zpos mx)). unfold emin in A. clear -A ; lia. * split. unfold emin in A |- * ; clear -A ; lia. replace ew with ((ew - 1) + 1)%Z by ring. rewrite Zpower_plus by (clear - Hew ; lia). unfold emin, emax in *. change (2^1)%Z with 2%Z. clear -B ; lia. + apply -> Z.lt_sub_0 in H. apply join_bits_range ; now split. Qed.
imports: Coq(ZArith Reals Lia SpecFloat) Core BinarySingleNaN Binary