proposition: Lemma join_bits_range : forall s m e, (0 <= m < 2^mw)%Z -> (0 <= e < 2^ew)%Z -> (0 <= join_bits s m e < 2 ^ (mw + ew + 1))%Z.
proof: Proof. intros s m e Hm He. assert (0 <= mw)%Z as Hmw. destruct mw as [|mw'|mw'] ; try easy. clear -Hm ; simpl in Hm ; lia. assert (0 <= ew)%Z as Hew. destruct ew as [|ew'|ew'] ; try easy. clear -He ; simpl in He ; lia. unfold join_bits. rewrite Z.shiftl_mul_pow2 by easy. split. - apply (Zplus_le_compat 0 _ 0) with (2 := proj1 Hm). rewrite <- (Zmult_0_l (2^mw)). apply Zmult_le_compat_r. case s. clear -He ; lia. now rewrite Zmult_0_l. clear -Hm ; lia. - apply Z.lt_le_trans with (((if s then 2 ^ ew else 0) + e + 1) * 2 ^ mw)%Z. rewrite (Zmult_plus_distr_l _ 1). apply Zplus_lt_compat_l. now rewrite Zmult_1_l. rewrite <- (Zplus_assoc mw), (Zplus_comm mw), Zpower_plus. apply Zmult_le_compat_r. rewrite Zpower_plus by easy. change (2^1)%Z with 2%Z. case s ; clear -He ; lia. clear -Hm ; lia. clear -Hew ; lia. easy. Qed.
imports: Coq(ZArith Reals Lia SpecFloat) Core BinarySingleNaN Binary