proposition: Lemma FLT_format_half: forall u, format u -> bpow (prec+emin) <= Rabs u -> format (u/2).
proof: Proof. Proof with auto with typeclass_instances. intros u Fu H. apply FLT_format_generic in Fu... destruct Fu as [[n e] H1 H2 H3]. simpl in H1, H2, H3. apply generic_format_FLT. exists (Float radix2 n (e-1)). rewrite H1; unfold F2R; simpl. unfold Zminus; rewrite bpow_plus. change (bpow (-(1))) with (/2). unfold Rdiv; ring. easy. cut (prec + emin < prec +e)%Z. simpl ; lia. apply lt_bpow with radix2. apply Rle_lt_trans with (1:=H). rewrite H1; unfold F2R; simpl. rewrite Rabs_mult; rewrite (Rabs_right (bpow e)). 2: apply Rle_ge, bpow_ge_0. rewrite bpow_plus. apply Rmult_lt_compat_r. apply bpow_gt_0. rewrite <- abs_IZR. rewrite <- IZR_Zpower. now apply IZR_lt. now apply Zlt_le_weak. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)