Fprop_plus_error.v 14.9 KB
Newer Older
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1
(**
2 3 4
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/

5
Copyright (C) 2010-2013 Sylvie Boldo
BOLDO Sylvie's avatar
BOLDO Sylvie committed
6
#<br />#
7
Copyright (C) 2010-2013 Guillaume Melquiond
8 9 10 11 12 13 14 15 16 17 18 19

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

20 21
(** * Error of the rounded-to-nearest addition is representable. *)

22
Require Import Psatz.
23 24 25 26
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_float_prop.
Require Import Fcore_generic_fmt.
27 28 29
Require Import Fcore_FIX.
Require Import Fcore_FLX.
Require Import Fcore_FLT.
30
Require Import Fcore_ulp.
31 32
Require Import Fcalc_ops.

33

34 35 36 37 38 39
Section Fprop_plus_error.

Variable beta : radix.
Notation bpow e := (bpow beta e).

Variable fexp : Z -> Z.
40
Context { valid_exp : Valid_exp fexp }.
41

42 43 44 45 46
Section round_repr_same_exp.

Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.

47
Theorem round_repr_same_exp :
48
  forall m e,
49
  exists m',
50
  round beta fexp rnd (F2R (Float beta m e)) = F2R (Float beta m' e).
51 52
Proof with auto with typeclass_instances.
intros m e.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
53
set (e' := canonic_exp beta fexp (F2R (Float beta m e))).
54
unfold round, scaled_mantissa. fold e'.
55 56 57
destruct (Zle_or_lt e' e) as [He|He].
exists m.
unfold F2R at 2. simpl.
58
rewrite Rmult_assoc, <- bpow_plus.
59
rewrite <- Z2R_Zpower. 2: omega.
60
rewrite <- Z2R_mult, Zrnd_Z2R...
61
unfold F2R. simpl.
62
rewrite Z2R_mult.
63 64
rewrite Rmult_assoc.
rewrite Z2R_Zpower. 2: omega.
65
rewrite <- bpow_plus.
66 67
apply (f_equal (fun v => Z2R m * bpow v)%R).
ring.
68
exists ((rnd (Z2R m * bpow (e - e'))) * Zpower beta (e' - e))%Z.
69
unfold F2R. simpl.
70
rewrite Z2R_mult.
71 72
rewrite Z2R_Zpower. 2: omega.
rewrite 2!Rmult_assoc.
73
rewrite <- 2!bpow_plus.
74 75 76 77
apply (f_equal (fun v => _ * bpow v)%R).
ring.
Qed.

78 79
End round_repr_same_exp.

80
Context { monotone_exp : Monotone_exp fexp }.
81 82
Notation format := (generic_format beta fexp).

83
Variable choice : Z -> bool.
84

85
Lemma plus_error_aux :
86
  forall x y,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
87
  (canonic_exp beta fexp x <= canonic_exp beta fexp y)%Z ->
88
  format x -> format y ->
89
  format (round beta fexp (Znearest choice) (x + y) - (x + y))%R.
90 91
Proof.
intros x y.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
92 93
set (ex := canonic_exp beta fexp x).
set (ey := canonic_exp beta fexp y).
94
intros He Hx Hy.
95
destruct (Req_dec (round beta fexp (Znearest choice) (x + y) - (x + y)) R0) as [H0|H0].
96 97 98 99 100
rewrite H0.
apply generic_format_0.
set (mx := Ztrunc (scaled_mantissa beta fexp x)).
set (my := Ztrunc (scaled_mantissa beta fexp y)).
(* *)
101
assert (Hxy: (x + y)%R = F2R (Float beta (mx + my * beta ^ (ey - ex)) ex)).
102 103
rewrite Hx, Hy.
fold mx my ex ey.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
104
rewrite <- F2R_plus.
105 106 107 108
unfold Fplus. simpl.
now rewrite Zle_imp_le_bool with (1 := He).
(* *)
rewrite Hxy.
109
destruct (round_repr_same_exp (Znearest choice) (mx + my * beta ^ (ey - ex)) ex) as (mxy, Hxy').
110
rewrite Hxy'.
111 112
assert (H: (F2R (Float beta mxy ex) - F2R (Float beta (mx + my * beta ^ (ey - ex)) ex))%R =
  F2R (Float beta (mxy - (mx + my * beta ^ (ey - ex))) ex)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
113
now rewrite <- F2R_minus, Fminus_same_exp.
114
rewrite H.
115 116
apply generic_format_F2R.
intros _.
117 118
apply monotone_exp.
rewrite <- H, <- Hxy', <- Hxy.
119
apply ln_beta_le_abs.
120 121 122
exact H0.
pattern x at 3 ; replace x with (-(y - (x + y)))%R by ring.
rewrite Rabs_Ropp.
123
now apply (round_N_pt beta _ choice (x + y)).
124 125
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
126
(** Error of the addition *)
127 128 129
Theorem plus_error :
  forall x y,
  format x -> format y ->
130
  format (round beta fexp (Znearest choice) (x + y) - (x + y))%R.
131 132
Proof.
intros x y Hx Hy.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
133
destruct (Zle_or_lt (canonic_exp beta fexp x) (canonic_exp beta fexp y)).
134 135 136 137 138 139
now apply plus_error_aux.
rewrite Rplus_comm.
apply plus_error_aux ; try easy.
now apply Zlt_le_weak.
Qed.

140 141 142 143 144 145 146 147
End Fprop_plus_error.

Section Fprop_plus_zero.

Variable beta : radix.
Notation bpow e := (bpow beta e).

Variable fexp : Z -> Z.
148
Context { valid_exp : Valid_exp fexp }.
149
Context { exp_not_FTZ : Exp_not_FTZ fexp }.
150 151
Notation format := (generic_format beta fexp).

152 153 154 155 156
Section round_plus_eq_zero_aux.

Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.

157
Lemma round_plus_eq_zero_aux :
158
  forall x y,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
159
  (canonic_exp beta fexp x <= canonic_exp beta fexp y)%Z ->
160 161
  format x -> format y ->
  (0 <= x + y)%R ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
162
  round beta fexp rnd (x + y) = 0%R ->
163
  (x + y = 0)%R.
164 165
Proof with auto with typeclass_instances.
intros x y He Hx Hy Hp Hxy.
166 167 168 169 170 171 172 173
destruct (Req_dec (x + y) 0) as [H0|H0].
exact H0.
destruct (ln_beta beta (x + y)) as (exy, Hexy).
simpl.
specialize (Hexy H0).
destruct (Zle_or_lt exy (fexp exy)) as [He'|He'].
(* . *)
assert (H: (x + y)%R = F2R (Float beta (Ztrunc (x * bpow (- fexp exy)) +
174
  Ztrunc (y * bpow (- fexp exy))) (fexp exy))).
175 176
rewrite (subnormal_exponent beta fexp exy x He' Hx) at 1.
rewrite (subnormal_exponent beta fexp exy y He' Hy) at 1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
177
now rewrite <- F2R_plus, Fplus_same_exp.
178
rewrite H in Hxy.
179
rewrite round_generic in Hxy...
180
now rewrite <- H in Hxy.
181 182
apply generic_format_F2R.
intros _.
183
rewrite <- H.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
184
unfold canonic_exp.
185 186 187
rewrite ln_beta_unique with (1 := Hexy).
apply Zle_refl.
(* . *)
188
elim Rle_not_lt with (1 := round_le beta _ rnd _ _ (proj1 Hexy)).
189 190
rewrite (Rabs_pos_eq _ Hp).
rewrite Hxy.
191
rewrite round_generic...
192 193
apply bpow_gt_0.
apply generic_format_bpow.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
194 195
apply Zlt_succ_le.
now rewrite (Zsucc_pred exy) in He'.
196 197
Qed.

198 199 200 201 202
End round_plus_eq_zero_aux.

Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
203
(** rnd(x+y)=0 -> x+y = 0 provided this is not a FTZ format *)
204
Theorem round_plus_eq_zero :
205
  forall x y,
206
  format x -> format y ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
207
  round beta fexp rnd (x + y) = 0%R ->
208
  (x + y = 0)%R.
209 210
Proof with auto with typeclass_instances.
intros x y Hx Hy.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
211
destruct (Rle_or_lt 0 (x + y)) as [H1|H1].
212 213
(* . *)
revert H1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
214
destruct (Zle_or_lt (canonic_exp beta fexp x) (canonic_exp beta fexp y)) as [H2|H2].
215
now apply round_plus_eq_zero_aux.
216
rewrite Rplus_comm.
217
apply round_plus_eq_zero_aux ; try easy.
218 219 220 221 222
now apply Zlt_le_weak.
(* . *)
revert H1.
rewrite <- (Ropp_involutive (x + y)), Ropp_plus_distr, <- Ropp_0.
intros H1.
223
rewrite round_opp.
224 225
intros Hxy.
apply f_equal.
226
cut (round beta fexp (Zrnd_opp rnd) (- x + - y) = 0)%R.
227
cut (0 <= -x + -y)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
228
destruct (Zle_or_lt (canonic_exp beta fexp (-x)) (canonic_exp beta fexp (-y))) as [H2|H2].
229
apply round_plus_eq_zero_aux ; try apply generic_format_opp...
230
rewrite Rplus_comm.
231
apply round_plus_eq_zero_aux ; try apply generic_format_opp...
232 233 234
now apply Zlt_le_weak.
apply Rlt_le.
now apply Ropp_lt_cancel.
235
rewrite <- (Ropp_involutive (round _ _ _ _)).
236 237 238 239 240
rewrite Hxy.
apply Ropp_involutive.
Qed.

End Fprop_plus_zero.
241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271

Section Fprop_plus_FLT.
Variable beta : radix.

Notation bpow e := (bpow beta e).

Variable emin prec : Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.

Theorem FLT_format_plus_small: forall x y,
  generic_format beta (FLT_exp emin prec) x ->
  generic_format beta (FLT_exp emin prec) y ->
   (Rabs (x+y) <= bpow (prec+emin))%R ->
    generic_format beta (FLT_exp emin prec) (x+y).
Proof with auto with typeclass_instances.
intros x y Fx Fy H.
apply generic_format_FLT_FIX...
rewrite Zplus_comm; assumption.
apply generic_format_FIX_FLT, FIX_format_generic in Fx.
apply generic_format_FIX_FLT, FIX_format_generic in Fy.
destruct Fx as (nx,(H1x,H2x)).
destruct Fy as (ny,(H1y,H2y)).
apply generic_format_FIX.
exists (Float beta (Fnum nx+Fnum ny)%Z emin).
split;[idtac|reflexivity].
rewrite H1x,H1y; unfold F2R; simpl.
rewrite H2x, H2y.
rewrite Z2R_plus; ring.
Qed.

End Fprop_plus_FLT.
272

273
Section Fprop_plus_mult_ulp.
274 275 276 277 278 279 280 281 282 283 284 285 286

Variable beta : radix.
Notation bpow e := (bpow beta e).

Variable fexp : Z -> Z.
Context { valid_exp : Valid_exp fexp }.
Context { monotone_exp : Monotone_exp fexp }.
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.

Notation format := (generic_format beta fexp).
Notation cexp := (canonic_exp beta fexp).

287 288 289
Lemma ex_shift :
  forall x e, format x -> (e <= cexp x)%Z ->
  exists m, (x = Z2R m * bpow e)%R.
290 291 292 293 294 295 296 297 298 299 300
Proof with auto with typeclass_instances.
intros x e Fx He.
exists (Ztrunc (scaled_mantissa beta fexp x)*Zpower beta (cexp x -e))%Z.
rewrite Fx at 1; unfold F2R; simpl.
rewrite Z2R_mult, Rmult_assoc.
f_equal.
rewrite Z2R_Zpower.
2: omega.
rewrite <- bpow_plus; f_equal; ring.
Qed.

301 302 303 304 305 306 307 308
Lemma ln_beta_minus1 :
  forall z, z <> 0%R ->
  (ln_beta beta z - 1)%Z = ln_beta beta (z / Z2R beta).
Proof.
intros z Hz.
unfold Zminus.
rewrite <- ln_beta_mult_bpow with (1 := Hz).
now rewrite bpow_opp, bpow_1.
309 310
Qed.

311 312 313
Theorem round_plus_mult_ulp :
  forall x y, format x -> format y -> (x <> 0)%R ->
  exists m, (round beta fexp rnd (x+y) = Z2R m * ulp beta fexp (x/Z2R beta))%R.
314 315
Proof with auto with typeclass_instances.
intros x y Fx Fy Zx.
316 317
case (Zle_or_lt (ln_beta beta (x/Z2R beta)) (ln_beta beta y)); intros H1.
pose (e:=cexp (x / Z2R beta)).
318
destruct (ex_shift x e) as (nx, Hnx); try exact Fx.
319
apply monotone_exp.
320 321
rewrite <- (ln_beta_minus1 x Zx); omega.
destruct (ex_shift y e) as (ny, Hny); try assumption.
322 323 324 325 326 327 328 329 330 331 332 333 334
apply monotone_exp...
destruct (round_repr_same_exp beta fexp rnd (nx+ny) e) as (n,Hn).
exists n.
apply trans_eq with (F2R (Float beta n e)).
rewrite <- Hn; f_equal.
rewrite Hnx, Hny; unfold F2R; simpl; rewrite Z2R_plus; ring.
unfold F2R; simpl.
rewrite ulp_neq_0; try easy.
apply Rmult_integral_contrapositive_currified; try assumption.
apply Rinv_neq_0_compat.
apply Rgt_not_eq.
apply radix_pos.
(* *)
335
destruct (ex_shift (round beta fexp rnd (x + y)) (cexp (x/Z2R beta))) as (n,Hn).
336 337 338
apply generic_format_round...
apply Zle_trans with (cexp (x+y)).
apply monotone_exp.
339
rewrite <- ln_beta_minus1 by easy.
340
rewrite <- (ln_beta_abs beta (x+y)).
341
(* . *)
342 343 344
assert (U: (Rabs (x+y) = Rabs x + Rabs y)%R \/ (y <> 0 /\ Rabs (x+y) = Rabs x - Rabs y)%R).
assert (V: forall x y, (Rabs y <= Rabs x)%R ->
   (Rabs (x+y) = Rabs x + Rabs y)%R \/ (y <> 0 /\ Rabs (x+y) = Rabs x - Rabs y)%R).
345 346 347 348
clear; intros x y.
case (Rle_or_lt 0 y); intros Hy.
case Hy; intros Hy'.
case (Rle_or_lt 0 x); intros Hx.
349 350 351 352 353 354
intros _; rewrite (Rabs_pos_eq y) by easy.
rewrite (Rabs_pos_eq x) by easy.
left; apply Rabs_pos_eq.
now apply Rplus_le_le_0_compat.
rewrite (Rabs_pos_eq y) by easy.
rewrite (Rabs_left x) by easy.
355 356 357 358 359 360 361 362
intros H; right; split.
now apply Rgt_not_eq.
rewrite Rabs_left1.
ring.
apply Rplus_le_reg_l with (-x)%R; ring_simplify; assumption.
intros _; left.
now rewrite <- Hy', Rabs_R0, 2!Rplus_0_r.
case (Rle_or_lt 0 x); intros Hx.
363 364
rewrite (Rabs_left y) by easy.
rewrite (Rabs_pos_eq x) by easy.
365
intros H; right; split.
366 367
now apply Rlt_not_eq.
rewrite Rabs_pos_eq.
368
ring.
369
apply Rplus_le_reg_l with (-y)%R; ring_simplify; assumption.
370
intros _; left.
371 372
rewrite (Rabs_left y) by easy.
rewrite (Rabs_left x) by easy.
373 374
rewrite Rabs_left1.
ring.
375
lra.
376 377 378 379 380 381
apply V; left.
apply ln_beta_lt_pos with beta.
now apply Rabs_pos_lt.
rewrite <- ln_beta_minus1 in H1; try assumption.
rewrite 2!ln_beta_abs; omega.
(* . *)
382
destruct U as [U|U].
383 384
rewrite U; apply Zle_trans with (ln_beta beta x).
omega.
385 386 387 388 389 390 391 392 393 394 395
rewrite <- ln_beta_abs.
apply ln_beta_le.
now apply Rabs_pos_lt.
apply Rplus_le_reg_l with (-Rabs x)%R; ring_simplify.
apply Rabs_pos.
destruct U as (U',U); rewrite U.
rewrite <- ln_beta_abs.
apply ln_beta_minus_lb.
now apply Rabs_pos_lt.
now apply Rabs_pos_lt.
rewrite 2!ln_beta_abs.
396
assert (ln_beta beta y < ln_beta beta x - 1)%Z.
397
now rewrite (ln_beta_minus1 x Zx).
398
omega.
399 400
apply canonic_exp_round_ge...
intros K.
401
apply round_plus_eq_zero in K...
402
contradict H1; apply Zle_not_lt.
403
rewrite <- (ln_beta_minus1 x Zx).
404 405
replace y with (-x)%R.
rewrite ln_beta_opp; omega.
406
lra.
407 408 409 410 411 412 413
exists n.
rewrite ulp_neq_0.
assumption.
apply Rmult_integral_contrapositive_currified; try assumption.
apply Rinv_neq_0_compat.
apply Rgt_not_eq.
apply radix_pos.
414 415
Qed.

416 417 418 419 420 421
Context {exp_not_FTZ : Exp_not_FTZ fexp}.

Theorem round_plus_ge_ulp :
  forall x y, format x -> format y ->
  round beta fexp rnd (x+y) = 0%R \/
  (ulp beta fexp (x/Z2R beta) <= Rabs (round beta fexp rnd (x+y)))%R.
422
Proof with auto with typeclass_instances.
423
intros x y Fx Fy.
424 425 426 427 428 429 430
case (Req_dec x 0); intros Zx.
(* *)
rewrite Zx, Rplus_0_l.
rewrite round_generic...
unfold Rdiv; rewrite Rmult_0_l.
rewrite Fy at 2.
unfold F2R; simpl; rewrite Rabs_mult.
431
rewrite (Rabs_pos_eq (bpow _)) by apply bpow_ge_0.
432 433 434 435 436 437 438 439 440 441
case (Z.eq_dec (Ztrunc (scaled_mantissa beta fexp y)) 0); intros Hm.
left.
rewrite Fy, Hm; unfold F2R; simpl; ring.
right.
apply Rle_trans with (1*bpow (cexp y))%R.
rewrite Rmult_1_l.
rewrite <- ulp_neq_0.
apply ulp_ge_ulp_0...
intros K; apply Hm.
rewrite K, scaled_mantissa_0.
442
apply (Ztrunc_Z2R 0).
443 444 445
apply Rmult_le_compat_r.
apply bpow_ge_0.
rewrite <- Z2R_abs.
446 447
apply (Z2R_le 1).
apply (Zlt_le_succ 0).
448 449
now apply Z.abs_pos.
(* *)
450
destruct (round_plus_mult_ulp x y Fx Fy Zx) as (m,Hm).
451 452 453 454 455
case (Z.eq_dec m 0); intros Zm.
left.
rewrite Hm, Zm; simpl; ring.
right.
rewrite Hm, Rabs_mult.
456
rewrite (Rabs_pos_eq (ulp _ _ _)) by apply ulp_ge_0.
457 458 459 460 461
apply Rle_trans with (1*ulp beta fexp (x/Z2R beta))%R.
right; ring.
apply Rmult_le_compat_r.
apply ulp_ge_0.
rewrite <- Z2R_abs.
462 463
apply (Z2R_le 1).
apply (Zlt_le_succ 0).
464 465
now apply Z.abs_pos.
Qed.
466

467 468 469 470
End Fprop_plus_mult_ulp.

Section Fprop_plus_ge_ulp.

471 472
Variable beta : radix.
Notation bpow e := (bpow beta e).
473

474 475 476 477
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
Variable emin prec : Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.
478

479 480 481 482 483
Theorem round_plus_ge_ulp_FLT : forall x y e,
  generic_format beta (FLT_exp emin prec) x -> generic_format beta (FLT_exp emin prec) y ->
  (bpow e <= Rabs x)%R ->
  round beta (FLT_exp emin prec) rnd (x+y) = 0%R \/
  (bpow (e - prec) <= Rabs (round beta (FLT_exp emin prec) rnd (x+y)))%R.
484 485
Proof with auto with typeclass_instances.
intros x y e Fx Fy He.
486 487 488 489 490
assert (Zx: x <> 0%R).
  contradict He.
  apply Rlt_not_le; rewrite He, Rabs_R0.
  apply bpow_gt_0.
case round_plus_ge_ulp with beta (FLT_exp emin prec) rnd x y...
491 492 493 494
intros H; right.
apply Rle_trans with (2:=H).
rewrite ulp_neq_0.
unfold canonic_exp.
495
rewrite <- ln_beta_minus1 by easy.
496 497 498 499 500 501 502 503 504 505 506 507
unfold FLT_exp; apply bpow_le.
apply Zle_trans with (2:=Z.le_max_l _ _).
destruct (ln_beta beta x) as (n,Hn); simpl.
assert (e < n)%Z; try omega.
apply lt_bpow with beta.
apply Rle_lt_trans with (1:=He).
now apply Hn.
apply Rmult_integral_contrapositive_currified; try assumption.
apply Rinv_neq_0_compat.
apply Rgt_not_eq.
apply radix_pos.
Qed.
508

509 510 511 512 513
Theorem round_plus_ge_ulp_FLX : forall x y e,
  generic_format beta (FLX_exp prec) x -> generic_format beta (FLX_exp prec) y ->
  (bpow e <= Rabs x)%R ->
  round beta (FLX_exp prec) rnd (x+y) = 0%R \/
  (bpow (e - prec) <= Rabs (round beta (FLX_exp prec) rnd (x+y)))%R.
514 515
Proof with auto with typeclass_instances.
intros x y e Fx Fy He.
516 517 518 519 520
assert (Zx: x <> 0%R).
  contradict He.
  apply Rlt_not_le; rewrite He, Rabs_R0.
  apply bpow_gt_0.
case round_plus_ge_ulp with beta (FLX_exp prec) rnd x y...
521 522 523 524
intros H; right.
apply Rle_trans with (2:=H).
rewrite ulp_neq_0.
unfold canonic_exp.
525
rewrite <- ln_beta_minus1 by easy.
526 527 528 529 530 531 532 533 534 535 536
unfold FLX_exp; apply bpow_le.
destruct (ln_beta beta x) as (n,Hn); simpl.
assert (e < n)%Z; try omega.
apply lt_bpow with beta.
apply Rle_lt_trans with (1:=He).
now apply Hn.
apply Rmult_integral_contrapositive_currified; try assumption.
apply Rinv_neq_0_compat.
apply Rgt_not_eq.
apply radix_pos.
Qed.
537

538
End Fprop_plus_ge_ulp.