Commit 4d8ec832 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Added variant of generic_format_bpow that uses properties of fexp to weaken the hypothesis.

parent d9fa8833
......@@ -96,7 +96,21 @@ rewrite Ztrunc_Z2R.
rewrite <- F2R_bpow.
rewrite F2R_change_exp with (1 := H).
now rewrite Zmult_1_l.
omega.
now apply Zle_minus_le_0.
Qed.
Theorem generic_format_bpow' :
forall e, (fexp e <= e)%Z ->
generic_format (bpow e).
Proof.
intros e He.
apply generic_format_bpow.
destruct (Zle_lt_or_eq _ _ He).
now apply valid_exp.
rewrite <- H.
apply valid_exp_.
rewrite H.
apply Zle_refl.
Qed.
Theorem generic_format_F2R :
......
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