Commit 68a4fd29 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Simplified proofs.

parent 96e32822
......@@ -55,11 +55,7 @@ apply Rle_lt_trans with (2 := Hxy).
destruct (ln_beta beta (x + y)) as (exy', Exy). simpl.
now apply Exy.
replace exy with (Fexp (Fplus beta fx fy)) by exact (f_equal Fexp Pxy).
unfold Fplus.
generalize (Falign_spec_exp beta fx fy).
case (Falign beta fx fy). simpl.
intros (p, q) z Hz.
rewrite Hz.
rewrite Fexp_Fplus.
simpl. clear -monotone_exp.
apply sym_eq.
destruct (Zmin_spec ex ey) as [(H1,H2)|(H1,H2)] ; rewrite H2.
......@@ -38,11 +38,8 @@ now apply Rle_lt_trans with (1:=proj1 a).
apply Zplus_le_reg_l with prec; ring_simplify.
apply (bpow_lt_bpow beta).
now apply Rle_lt_trans with (1:=proj1 a).
rewrite <- Falign_spec_exp.
generalize (f_equal Fexp Hz).
unfold Fplus.
destruct (Falign beta fx fy) as ((p,q),t).
apply Zeq_le.
rewrite <- Fexp_Fplus, Hz.
apply Zle_refl.
Theorem format_nx: forall x, format x -> exists fx:float beta, (x=F2R fx)%R /\ Fexp fx = cexp x.
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