proposition: Theorem abs_B2R_ge_emin : forall x, is_finite_strict x = true -> (bpow radix2 emin <= Rabs (B2R x))%R.
proof: Proof. intros [sx|sx| |sx mx ex Hx] ; simpl ; try discriminate. intros; case sx; simpl. - unfold F2R; simpl; rewrite Rabs_mult, <-abs_IZR; simpl. rewrite Rabs_pos_eq; [|apply bpow_ge_0]. now apply bounded_ge_emin. - unfold F2R; simpl; rewrite Rabs_mult, <-abs_IZR; simpl. rewrite Rabs_pos_eq; [|apply bpow_ge_0]. now apply bounded_ge_emin. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative