proposition: Lemma generic_format_pred_aux2 : forall x, (0 < x)%R -> F x -> let e := mag_val beta x (mag beta x) in x = bpow (e - 1) -> F (x - bpow (fexp (e - 1))).
proof: Proof. intros x Zx Fx e Hx. pose (f:=(x - bpow (fexp (e - 1)))%R). fold f. assert (He:(fexp (e-1) <= e-1)%Z). apply generic_format_bpow_inv with beta; trivial. rewrite <- Hx; assumption. case (Zle_lt_or_eq _ _ He); clear He; intros He. assert (f = F2R (Float beta (Zpower beta (e-1-(fexp (e-1))) -1) (fexp (e-1))))%R. unfold f; rewrite Hx. unfold F2R; simpl. rewrite minus_IZR, IZR_Zpower. rewrite Rmult_minus_distr_r, Rmult_1_l. rewrite <- bpow_plus. now replace (e - 1 - fexp (e - 1) + fexp (e - 1))%Z with (e-1)%Z by ring. lia. rewrite H. apply generic_format_F2R. intros _. apply Zeq_le. apply cexp_fexp. rewrite <- H. unfold f; rewrite Hx. rewrite Rabs_right. split. apply Rplus_le_reg_l with (bpow (fexp (e-1))). ring_simplify. apply Rle_trans with (bpow (e - 2) + bpow (e - 2))%R. apply Rplus_le_compat ; apply bpow_le ; lia. apply Rle_trans with (2*bpow (e - 2))%R;[right; ring|idtac]. apply Rle_trans with (bpow 1*bpow (e - 2))%R. apply Rmult_le_compat_r. apply bpow_ge_0. replace (bpow 1) with (IZR beta). apply IZR_le. apply <- Zle_is_le_bool. now destruct beta. simpl. unfold Zpower_pos; simpl. now rewrite Zmult_1_r. rewrite <- bpow_plus. replace (1+(e-2))%Z with (e-1)%Z by ring. now right. rewrite <- Rplus_0_r. apply Rplus_lt_compat_l. rewrite <- Ropp_0. apply Ropp_lt_contravar. apply bpow_gt_0. apply Rle_ge; apply Rle_0_minus. apply bpow_le. lia. replace f with 0%R. apply generic_format_0. unfold f. rewrite Hx, He. ring. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop