proposition: Lemma FLXN_le_exp: forall f1 f2:float beta, ((Zpower beta (prec - 1) <= Z.abs (Fnum f1) < Zpower beta prec)%Z) -> ((Zpower beta (prec - 1) <= Z.abs (Fnum f2) < Zpower beta prec))%Z -> 0 <= F2R f1 -> F2R f1 <= F2R f2 -> (Fexp f1 <= Fexp f2)%Z.
proof: Proof. intros f1 f2 H1 H2 H3 H4. case (Zle_or_lt (Fexp f1) (Fexp f2)). trivial. assert (F2R f1 <= F2R f2) by assumption. intros H5; contradict H. apply Rlt_not_le. unfold F2R. apply Rlt_le_trans with (IZR(Zpower beta prec)*bpow (Fexp f2))%R. apply Rmult_lt_compat_r. apply bpow_gt_0. apply IZR_lt. apply Z.le_lt_trans with (2:=proj2 H2). rewrite Z.abs_eq. auto with zarith. apply le_IZR. apply Rmult_le_reg_r with (bpow (Fexp f2)). apply bpow_gt_0. rewrite Rmult_0_l. apply Rle_trans with (1:=H3). apply H4. rewrite IZR_Zpower, <-bpow_plus. apply Rle_trans with (bpow ((prec-1)+Fexp f1)). apply bpow_le. lia. rewrite bpow_plus. apply Rmult_le_compat_r. apply bpow_ge_0. rewrite <- IZR_Zpower. apply IZR_le. apply Z.le_trans with (1:=proj1 H1). rewrite Z.abs_eq. auto with zarith. apply le_IZR. apply Rmult_le_reg_r with (bpow (Fexp f1)). apply bpow_gt_0. rewrite Rmult_0_l. exact H3. lia. lia. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)