proposition: Lemma generic_format_round_pos : forall x, (0 < x)%R -> generic_format (round x).
proof: Proof. intros x Hx0. destruct (mag beta x) as (ex, Hex). specialize (Hex (Rgt_not_eq _ _ Hx0)). rewrite Rabs_pos_eq in Hex. 2: now apply Rlt_le. destruct (Zle_or_lt ex (fexp ex)) as [He|He]. destruct (round_bounded_small_pos _ _ He Hex) as [Hr|Hr] ; rewrite Hr. apply generic_format_0. apply generic_format_bpow. now apply valid_exp. generalize (round_bounded_large_pos _ _ He Hex). intros (Hr1, Hr2). destruct (Rle_or_lt (bpow ex) (round x)) as [Hr|Hr]. rewrite <- (Rle_antisym _ _ Hr Hr2). apply generic_format_bpow. now apply valid_exp. apply generic_format_F2R. intros _. rewrite (cexp_fexp_pos (F2R _) _ (conj Hr1 Hr)). rewrite (cexp_fexp_pos _ _ Hex). now apply Zeq_le. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop