Commit 8feaf946 authored by Sylvie Boldo's avatar Sylvie Boldo

Useless hypothesis

parent f02828f5
......@@ -115,11 +115,14 @@ apply generic_format_FLT.
Qed.
Theorem canonic_exp_FLT_FLX :
forall x, x <> R0 ->
forall x,
(bpow (emin + prec - 1) <= Rabs x)%R ->
canonic_exp beta FLT_exp x = canonic_exp beta (FLX_exp prec) x.
Proof.
intros x Hx0 Hx.
intros x Hx.
assert (Hx0: x <> 0%R).
intros H1; rewrite H1, Rabs_R0 in Hx.
contradict Hx; apply Rlt_not_le, bpow_gt_0.
unfold canonic_exp.
apply Zmax_left.
destruct (ln_beta beta x) as (ex, He).
......@@ -166,10 +169,6 @@ Theorem round_FLT_FLX : forall rnd x,
intros rnd x Hx.
unfold round, scaled_mantissa.
rewrite canonic_exp_FLT_FLX ; trivial.
contradict Hx.
rewrite Hx, Rabs_R0.
apply Rlt_not_le.
apply bpow_gt_0.
Qed.
(** Links between FLT and FIX (underflow) *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment