proposition: Lemma Expbe1: (Fexp be1 <= Fexp r1+1)%Z.
proof: Proof. assert (radix*r1=(Float (Fnum r1) (Fexp r1+1)))%R. unfold FtoRradix, FtoR; simpl; rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl; ring. apply Z.le_trans with (Fexp (Float (Fnum r1) (Fexp r1+1))); auto with zarith. apply Fcanonic_Rle_Zle with radix bo p; auto with zarith. left; auto. elim Nr1; intros J1 J2; elim J1; intros J3 J4. left; split;[split|idtac]; simpl; auto with zarith. fold FtoRradix; rewrite <- H. rewrite Rabs_mult; rewrite (Rabs_right radix). 2: apply Rle_ge, IZR_le; auto with real zarith. apply Rle_trans with (2*Rabs r1)%R. 2: apply Rmult_le_compat_r; auto with real. 2: apply Rabs_pos. 2: apply IZR_le; auto with real zarith. unfold FtoRradix; apply xLe2y with bo p u1 al1 al2; auto with real. apply Rle_trans with (Rabs u2). unfold FtoRradix; apply TwoSumProp with bo y al1; auto. apply Rmult_le_reg_l with 2%R; auto with real zarith. apply Rle_trans with (Fulp bo radix p u1);[idtac|simpl; right; field; auto with real]. rewrite u2Def; unfold FtoRradix; apply ClosestUlp; auto with zarith. apply Rmult_le_reg_l with 2%R; auto with real zarith. apply Rle_trans with (Fulp bo radix p al1);[idtac|simpl; right; field; auto with real]. fold FtoRradix; rewrite al2Def; unfold FtoRradix; apply ClosestUlp; auto with zarith. fold FtoRradix; replace (u1+al1+al2)%R with (a*x+y)%R; auto. rewrite al2Def; rewrite u2Def; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz