proposition: Theorem float_distribution_pos : forall m1 e1 m2 e2 : Z, (0 < m1)%Z -> (F2R (Float beta m1 e1) < F2R (Float beta m2 e2) < F2R (Float beta (m1 + 1) e1))%R -> (e2 < e1)%Z /\ (e1 + mag beta (IZR m1) = e2 + mag beta (IZR m2))%Z.
proof: Proof. intros m1 e1 m2 e2 Hp1 (H12, H21). assert (He: (e2 < e1)%Z). apply Znot_ge_lt. intros H0. elim Rlt_not_le with (1 := H21). apply Z.ge_le in H0. apply (F2R_change_exp e1 m2 e2) in H0. rewrite H0. apply F2R_le. apply Zlt_le_succ. apply (lt_F2R e1). now rewrite <- H0. split. exact He. rewrite (Zplus_comm e1), (Zplus_comm e2). assert (Hp2: (0 < m2)%Z). apply (gt_0_F2R m2 e2). apply Rlt_trans with (2 := H12). now apply F2R_gt_0. rewrite <- 2!mag_F2R. destruct (mag beta (F2R (Float beta m1 e1))) as (e1', H1). simpl. apply sym_eq. apply mag_unique. assert (H2 : (bpow (e1' - 1) <= F2R (Float beta m1 e1) < bpow e1')%R). rewrite <- (Z.abs_eq m1), F2R_Zabs. apply H1. apply Rgt_not_eq. apply Rlt_gt. now apply F2R_gt_0. now apply Zlt_le_weak. clear H1. rewrite <- F2R_Zabs, Z.abs_eq. split. apply Rlt_le. apply Rle_lt_trans with (2 := H12). apply H2. apply Rlt_le_trans with (1 := H21). now apply F2R_p1_le_bpow. now apply Zlt_le_weak. apply sym_not_eq. now apply Zlt_not_eq. apply sym_not_eq. now apply Zlt_not_eq. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits