proposition: Lemma F2R_ge: forall (y:float beta), (F2R y <> 0)%R -> (bpow (Fexp y) <= Rabs (F2R y))%R.
proof: Proof. intros (ny,ey). rewrite <- F2R_Zabs; unfold F2R; simpl. case (Zle_lt_or_eq 0 (Z.abs ny)). apply Z.abs_nonneg. intros Hy _. rewrite <- (Rmult_1_l (bpow _)) at 1. apply Rmult_le_compat_r. apply bpow_ge_0. apply IZR_le; lia. intros H1 H2; contradict H2. replace ny with 0%Z. simpl; ring. now apply sym_eq, Z.abs_0_iff, sym_eq. Qed.
imports: Coq(ZArith Reals Lia) Core Operations Plus_error