Library Float.Expansions.ThreeSum2

Require Export AllFloat.
Section F2.
Variable b : Fbound.
Variable precision : nat.

Let radix := 2%Z.

Coercion Local FtoRradix := FtoR radix.

Let TMTO : (1 < radix)%Z := TwoMoreThanOne.
Hint Resolve TMTO: zarith.
Hypothesis precisionNotZero : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
Variables p q r u v w p' q' r' : float.
Hypothesis Fp : Fbounded b p.
Hypothesis Fq : Fbounded b q.
Hypothesis Fr : Fbounded b r.
Hypothesis Fu : Fbounded b u.
Hypothesis Fv : Fbounded b v.
Hypothesis Fw : Fbounded b w.
Hypothesis Fp' : Fbounded b p'.
Hypothesis Fq' : Fbounded b q'.
Hypothesis Fr' : Fbounded b r'.
Hypothesis epq : (Fexp q <= Fexp p)%Z.
Hypothesis eqr : (Fexp r <= Fexp q)%Z.
Hypothesis uDef : Closest b radix (q + r) u.
Hypothesis vDef : v = (q + r - u)%R :>R.
Hypothesis p'Def : Closest b radix (p + u) p'.
Hypothesis wDef : w = (p + u - p')%R :>R.
Hypothesis q'Def : Closest b radix (w + v) q'.
Hypothesis r'Def : r' = (w + v - q')%R :>R.

Theorem TwoSumNul :
 forall f g x : float,
 Closest b radix (f + g) x ->
 x = 0%R :>R -> Fbounded b f -> Fbounded b g -> (f + g - x)%R = 0%R.
intros f g x H H0 H1 H2.
replace (FtoRradix f + FtoRradix g - FtoRradix x)%R with
 (FtoRradix f + FtoRradix g)%R; [ idtac | rewrite H0; ring ].
replace 0%R with (FtoRradix (Fzero (- dExp b)));
 [ idtac | unfold FtoRradix, FtoR in |- *; simpl in |- *; ring ].
apply sym_eq; apply (plusExact1 b radix) with (precision := precision);
 auto with arith.
cut (CompatibleP b radix (Closest b radix));
 [ intros Cp | apply ClosestCompatible; auto ].
apply Cp with (r1 := (f + g)%R) (p := x); auto with real.
fold FtoRradix in |- *; rewrite H0; unfold FtoRradix, FtoR in |- *;
 simpl in |- *; ring.
repeat split; simpl in |- *; auto with zarith.
simpl in |- *; apply Zmin_Zle; auto with float.
Qed.

Theorem bound3Sum :
 r' <> 0%R :>R ->
 (Rabs (q' + r') < 3%nat * radix * / pPred (vNum b) * Rabs p')%R.
intros H'; case (Req_dec w 0); intros Hw.
Contradict H'.
rewrite r'Def; auto.
rewrite Hw; rewrite Rplus_0_l.
apply Rminus_diag_eq.
unfold FtoRradix in |- *; apply ClosestIdem with (b := b); auto.
replace (FtoR radix v) with (w + v)%R; auto.
rewrite Hw; rewrite Rplus_0_l; auto.
rewrite r'Def; rewrite Rplus_minus.
apply Rle_lt_trans with (1 := Rabs_triang w v).
apply
 Rlt_le_trans
  with
    (3%nat * radix * / pPred (vNum b) * (/ radix * Rmax (Rabs p) (Rabs u)))%R.
replace (3%nat * radix * / pPred (vNum b))%R with
 (radix * radix * / pPred (vNum b) + radix * / pPred (vNum b))%R;
 [ idtac | simpl in |- *; ring ].
rewrite (fun x y : R => Rmult_comm x (/ radix * y));
 rewrite Rmult_plus_distr_l;
 repeat rewrite (fun y : R => Rmult_comm (/ radix * y)).
apply Rplus_lt_compat.
replace
 (radix * radix * / pPred (vNum b) * (/ radix * Rmax (Rabs p) (Rabs u)))%R
 with
 (radix * / radix * (radix * / pPred (vNum b) * Rmax (Rabs p) (Rabs u)))%R;
 [ rewrite Rinv_r; auto with real zarith; try rewrite Rmult_1_l | ring ].
rewrite wDef.
rewrite <- Ropp_minus_distr; rewrite Rabs_Ropp.
apply (plusErrorBound2 b precision); auto.
Contradict Hw.
rewrite wDef.
apply Rminus_diag_eq.
unfold FtoRradix in |- *; rewrite (is_Fzero_rep1 radix _ Hw); auto.
rewrite <- (FzeroisZero radix b).
apply sym_eq; apply (plusExact1 b radix precision); auto.
apply
 (ClosestCompatible b radix (p + u)%R (FtoR radix p + FtoR radix u)%R p');
 auto.
rewrite FzeroisZero; apply is_Fzero_rep1; auto.
apply FboundedFzero; auto.
simpl in |- *; unfold Zmin in |- *; case (Fexp p ?= Fexp u)%Z;
 auto with float.
apply Rlt_le_trans with (radix * / pPred (vNum b) * (/ radix * Rabs u))%R.
rewrite vDef.
rewrite <- Ropp_minus_distr; rewrite Rabs_Ropp.
replace (radix * / pPred (vNum b) * (/ radix * Rabs u))%R with
 (Rabs u * / radix * (radix * / pPred (vNum b)))%R;
 [ idtac | ring ].
unfold FtoRradix in |- *; apply (plusErrorBound1 b radix precision); auto.
Contradict Hw.
rewrite wDef.
unfold FtoRradix in |- *; rewrite (is_Fzero_rep1 radix _ Hw).
rewrite Rplus_0_r.
apply Rminus_diag_eq.
unfold FtoRradix in |- *; apply ClosestIdem with (b := b); auto.
replace (FtoR radix p) with (p + u)%R; auto.
unfold FtoRradix in |- *; rewrite (is_Fzero_rep1 radix _ Hw).
rewrite Rplus_0_r; auto.
apply Rmult_le_compat_l; auto with real.
replace 0%R with (radix * 0)%R; auto with real; apply Rmult_le_compat_l;
 auto with real arith.
apply Rlt_le; apply Rinv_0_lt_compat; auto with real arith.
apply Rlt_IZRO.
apply (pPredMoreThanOne b radix precision); auto with arith.
apply Rmult_le_compat_l; auto with real arith.
apply RmaxLess2; auto.
apply Rmult_le_compat_l; auto with real arith.
replace 0%R with (3%nat * radix * 0)%R; auto with real;
 apply Rmult_le_compat_l; auto with real arith.
replace (3%nat * radix)%R with (INR 6); [ idtac | simpl in |- *; ring ].
replace 0%R with (INR 0); auto with real arith.
apply Rlt_le; apply Rinv_0_lt_compat; auto with real arith.
apply Rlt_IZRO.
apply (pPredMoreThanOne b radix precision); auto with arith.
apply (plusClosestLowerBound b precision); auto with real.
Contradict Hw.
rewrite wDef.
unfold FtoRradix, radix in |- *; rewrite Hw; ring.
Qed.

Theorem exp3Sum :
 exists p'' : float,
   (exists q'' : float,
      (exists r'' : float,
         (Fbounded b p'' /\ Fbounded b q'' /\ Fbounded b r'') /\
         (p'' = p' :>R /\ q'' = q' :>R /\ r'' = r' :>R) /\
         (Fexp r <= Fexp r'')%Z /\
         ((Fexp r'' <= Fexp q'')%Z /\ (Fexp q'' <= Fexp p'')%Z) /\
         Fexp r'' = Fexp r)).
cut (Fbounded b (Fzero (Fexp r))); [ intros Fbr | apply FboundedZeroSameExp ];
 auto.
case (Req_dec v 0); intros Hv.
cut (Fzero (Fexp r) = r' :>R);
 [ intros EqZr
 | rewrite (FzeroisReallyZero radix); rewrite r'Def; rewrite Hv;
    rewrite Rplus_0_r; apply sym_eq; apply Rminus_diag_eq;
    unfold FtoRradix in |- *; apply (ClosestIdem b radix);
    auto; apply (ClosestCompatible b radix (w + v)%R w q');
    auto; rewrite Hv; ring ].
case (plusExpMin b radix precision) with (P := Closest b radix) (5 := uDef);
 auto.
apply ClosestRoundedModeP with (precision := precision); auto.
intros u' (H'0, (H'2, H'3)).
case (Req_dec w 0); intros Hw.
case
 (plusExpMin b radix precision)
  with (P := Closest b radix) (p := p) (q := u') (pq := p');
 auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply
 (ClosestCompatible b radix (p + u)%R (FtoR radix p + FtoR radix u')%R p');
 auto.
rewrite H'2; auto.
intros p'' (H'1, (H'5, H'6)).
exists p''; exists (Fzero (Fexp r)); exists (Fzero (Fexp r)); split;
 [ idtac | split ]; (split; [ idtac | split ]); auto.
rewrite (FzeroisReallyZero radix); auto.
rewrite <- (FzeroisZero radix b).
unfold FtoRradix in |- *; apply (ClosestIdem b radix); auto.
apply FboundedFzero; auto.
apply (ClosestCompatible b radix (w + v)%R (Fzero (- dExp b)) q'); auto.
rewrite Hw; rewrite Hv; unfold FtoRradix in |- *;
 rewrite (FzeroisZero radix b); ring.
simpl in |- *; auto with zarith.
split; simpl in |- *; auto with zarith.
simpl in |- *.
apply Zle_trans with (2 := H'6).
apply Zmin_Zle; auto.
apply Zle_trans with (Fexp q); auto.
rewrite <- (Zmin_le2 (Fexp q) (Fexp r)); auto.
case (errorBoundedPlus b radix precision) with (p := p) (q := u') (pq := p');
 auto.
apply
 (ClosestCompatible b radix (p + u)%R (FtoR radix p + FtoR radix u')%R p');
 auto.
rewrite H'2; auto.
intros w' (H'1, (H'5, H'6)).
exists p'; exists w'; exists (Fzero (Fexp r)); split; [ idtac | split ];
 (split; [ idtac | split ]); auto.
unfold FtoRradix in |- *; apply (ClosestIdem b radix); auto.
apply (ClosestCompatible b radix (w + v)%R (FtoR radix w') q'); auto.
rewrite Hv; rewrite Rplus_0_r; auto.
rewrite wDef; unfold FtoRradix in |- *; rewrite <- H'2; auto.
simpl in |- *; auto with zarith.
split; simpl in |- *; auto with zarith.
simpl in |- *; rewrite H'6.
apply Zmin_Zle; auto.
apply Zle_trans with (Fexp q); auto.
apply Zle_trans with (2 := H'3); auto with zarith.
rewrite Zmin_le2; auto with zarith.
rewrite H'6.
apply Zlt_le_weak.
apply (plusExact1bis b radix precision); auto.
apply
 (ClosestCompatible b radix (p + u)%R (FtoR radix p + FtoR radix u')%R p');
 auto.
rewrite H'2; auto.
Contradict Hw.
rewrite wDef; auto.
unfold FtoRradix in |- *; rewrite <- H'2.
rewrite <- Hw; ring; ring.
case (Req_dec w 0); intros Hw.
cut (Fzero (Fexp r) = r' :>R);
 [ intros EqZr
 | rewrite (FzeroisReallyZero radix); rewrite r'Def; rewrite Hw;
    rewrite Rplus_0_l; apply sym_eq; apply Rminus_diag_eq;
    unfold FtoRradix in |- *; apply (ClosestIdem b radix);
    auto; apply (ClosestCompatible b radix (w + v)%R (FtoR radix v) q');
    auto; rewrite Hw; unfold FtoRradix in |- *; ring ].
case (plusExpMin b radix precision) with (P := Closest b radix) (5 := uDef);
 auto.
apply ClosestRoundedModeP with (precision := precision); auto.
intros u' (H'0, (H'2, H'3)).
case (errorBoundedPlus b radix precision) with (p := q) (q := r) (pq := u');
 auto.
apply
 (ClosestCompatible b radix (FtoR radix q + FtoR radix r)%R
    (FtoR radix q + FtoR radix r)%R u); auto.
intros v' H'; elim H'; intros H'1 H'4; elim H'4; intros H'5 H'6; clear H'4 H'.
case
 (plusExpMin b radix precision)
  with (P := Closest b radix) (p := p) (q := u') (pq := p');
 auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply
 (ClosestCompatible b radix (p + u)%R (FtoR radix p + FtoR radix u')%R p');
 auto.
rewrite H'2; auto.
intros p'' (H'4, (H'8, H'9)).
exists p''; exists v'; exists (Fzero (Fexp r)); split; [ idtac | split ];
 (split; [ idtac | split ]); auto.
replace (FtoRradix v') with (FtoRradix v); [ idtac | rewrite vDef; auto ].
unfold FtoRradix in |- *; apply (ClosestIdem b radix); auto;
 apply (ClosestCompatible b radix (w + v)%R (FtoR radix v) q');
 auto; rewrite Hw; unfold FtoRradix in |- *; ring.
unfold FtoRradix in |- *; rewrite H'1; auto.
rewrite H'2; auto.
simpl in |- *; auto with zarith.
split; simpl in |- *; auto with zarith.
rewrite H'6; rewrite Zmin_le2; auto with zarith.
apply Zle_trans with (2 := H'9).
apply Zmin_Zle; auto.
rewrite H'6; auto.
apply Zle_trans with (Fexp q); auto with zarith.
rewrite H'6; auto.
case (plusExpMin b radix precision) with (P := Closest b radix) (5 := uDef);
 auto.
apply ClosestRoundedModeP with (precision := precision); auto.
intros u' (H'0, (H'2, H'3)).
case (errorBoundedPlus b radix precision) with (p := q) (q := r) (pq := u');
 auto.
apply
 (ClosestCompatible b radix (FtoR radix q + FtoR radix r)%R
    (FtoR radix q + FtoR radix r)%R u); auto.
intros v' H'; elim H'; intros H'1 H'4; elim H'4; intros H'5 H'6; clear H'4 H'.
case (errorBoundedPlus b radix precision) with (p := p) (q := u') (pq := p');
 auto.
apply
 (ClosestCompatible b radix (p + u)%R (FtoR radix p + FtoR radix u')%R p');
 auto.
rewrite H'2; auto.
intros w' (H'4, (H'8, H'9)).
case
 (plusExpBound b radix precision)
  with (P := Closest b radix) (p := w') (q := v') (pq := q');
 auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply
 (ClosestCompatible b radix (w + v)%R (FtoR radix w' + FtoR radix v')%R q');
 auto.
rewrite wDef; unfold FtoRradix in |- *; rewrite H'4; auto.
unfold FtoRradix in vDef; rewrite vDef; unfold FtoRradix in |- *;
 rewrite <- H'2; rewrite H'1; auto.
intros q'' (H'7, (H'11, (H'13, H'14))).
case
 (errorBoundedPlus b radix precision) with (p := v') (q := w') (pq := q'');
 auto.
apply
 (ClosestCompatible b radix (w + v)%R (FtoR radix v' + FtoR radix w')%R q');
 auto.
rewrite wDef; rewrite vDef; rewrite H'4; rewrite H'1;
 unfold FtoRradix in |- *; repeat rewrite H'2; ring;
 ring.
intros r'' (H'10, (H'15, H'16)).
exists p'; exists q''; exists r''; split; [ idtac | split ];
 (split; [ idtac | split ]); auto.
rewrite r'Def; rewrite wDef; rewrite vDef; unfold FtoRradix in |- *;
 rewrite H'10; rewrite H'4; rewrite H'1; repeat rewrite H'2;
 rewrite H'11; ring; ring.
rewrite H'16; apply Zmin_Zle; auto with zarith.
rewrite H'6; apply Zmin_Zle; auto with zarith.
rewrite H'9; apply Zmin_Zle; auto with zarith.
apply Zle_trans with (2 := H'3); apply Zmin_Zle; auto with zarith.
split.
rewrite H'16; rewrite Zmin_sym; auto.
apply Zle_trans with (1 := H'14).
rewrite Zmax_le1; auto.
apply Zlt_le_succ; auto.
rewrite H'9.
apply plusExact1bis with (b := b) (radix := radix) (precision := precision);
 auto.
apply
 (ClosestCompatible b radix (p + u)%R (FtoR radix p + FtoR radix u')%R p');
 auto.
rewrite H'2; auto.
Contradict Hw; auto.
rewrite wDef; auto.
unfold FtoRradix in |- *; rewrite <- H'2.
rewrite <- Hw; ring; ring.
rewrite H'9.
apply Zmin_Zle; auto.
rewrite H'6; rewrite Zmin_le2; auto with zarith.
rewrite H'6; auto.
rewrite H'16.
rewrite H'6.
rewrite H'9.
replace (Zmin (Fexp q) (Fexp r)) with (Fexp r).
apply Zmin_le1.
apply Zmin_Zle; auto.
apply Zle_trans with (Fexp q); auto.
rewrite <- (Zmin_le2 (Fexp q) (Fexp r)); auto.
apply sym_eq; apply Zmin_le2; auto.
Qed.

Theorem OutSum3 :
 r' <> 0%R :>R ->
 (Float 1%nat (Fexp r) <
  3%nat *
  (radix *
   (radix * (Rabs p' * / (pPred (vNum b) * (radix * pPred (vNum b) - radix))))))%R.
intros H; case exp3Sum;
 intros p''
  (q'',
   (r'', ((H'1, (H'2, H'3)), ((H'4, (H'5, H'6)), (H'7, ((H'8, H'9), H'10)))))).
cut (~ is_Fzero q'); [ intros Z1 | idtac ].
2: Contradict H; auto with real float.
2: replace (FtoRradix r') with (w + v - q')%R; auto.
2: apply TwoSumNul; auto.
2: unfold is_Fzero in H.
2: unfold FtoRradix, FtoR in |- *.
2: replace (Fnum q') with 0%Z; simpl; ring.
apply Rle_lt_trans with (Rabs r'').
apply Rle_trans with (FtoR radix (Float 1%nat (Fexp r''))).
unfold FtoRradix in |- *.
replace (Fexp r) with (Fexp r''); auto with real.
rewrite <- (Fabs_correct radix); auto with arith.
apply Fop.RleFexpFabs; auto with arith.
fold FtoRradix in |- *.
rewrite H'6; auto.
apply Rlt_trans with (Rabs q' * / radix * (radix * / pPred (vNum b)))%R.
replace (FtoRradix r'') with (w + v - q')%R.
replace (Rabs (w + v - q')) with (Rabs (q' - (w + v))).
apply
 plusErrorBound1
  with (b := b) (radix := radix) (precision := precision) (p := w) (q := v);
 auto with arith.
apply Rabs_minus_sym.
rewrite H'6; auto.
cut
 ((Rabs q' <
   3%nat * (radix * (Rabs p' * / pPred (vNum b))) +
   Rabs q' * / pPred (vNum b))%R ->
  (Rabs q' * / radix * (radix * / pPred (vNum b)) <
   3%nat *
   (radix *
    (radix *
     (Rabs p' * / (pPred (vNum b) * (radix * pPred (vNum b) - radix))))))%R).
intros C; apply C.
apply
 Rlt_trans with (3%nat * (radix * (Rabs p' * / pPred (vNum b))) + Rabs r')%R.
apply Rle_lt_trans with (Rabs (q' + r') + Rabs r')%R.
replace (Rabs q') with (Rabs (q' + r' + - r')).
replace (Rabs r') with (Rabs (- r')).
apply Rabs_triang.
apply Rabs_Ropp.
replace (q' + r' + - r')%R with (FtoRradix q'); [ auto | ring ].
replace (Rabs (q' + r') + Rabs r')%R with (Rabs r' + Rabs (q' + r'))%R;
 [ auto | ring ].
replace (3%nat * (radix * (Rabs p' * / pPred (vNum b))) + Rabs r')%R with
 (Rabs r' + 3%nat * (radix * (Rabs p' * / pPred (vNum b))))%R;
 [ auto | ring ].
apply Rplus_lt_compat_l.
replace (3%nat * (radix * (Rabs p' * / pPred (vNum b))))%R with
 (3%nat * radix * / pPred (vNum b) * Rabs p')%R; [ auto | ring ].
apply bound3Sum; auto.
apply Rplus_lt_compat_l.
replace (FtoRradix r') with (w + v - q')%R; auto.
replace (Rabs (FtoRradix w + FtoRradix v - FtoRradix q')) with
 (Rabs (q' - (w + v))).
replace (Rabs q' * / pPred (vNum b))%R with
 (Rabs q' * / radix * (radix * / pPred (vNum b)))%R.
apply
 plusErrorBound1
  with
    (b := b)
    (radix := radix)
    (precision := precision)
    (r := q')
    (p := w)
    (q := v); auto.
replace (Rabs (FtoRradix q') * / radix * (radix * / pPred (vNum b)))%R with
 (Rabs (FtoRradix q') * (/ radix * radix) * / pPred (vNum b))%R;
 [ rewrite Rinv_l; auto with real zarith | idtac ];
 ring.
replace (q' - (w + v))%R with (- (w + v - q'))%R;
 [ rewrite Rabs_Ropp | idtac ]; ring.
intros H'0.
replace (Rabs q' * / radix * (radix * / pPred (vNum b)))%R with
 (radix * / radix * (/ pPred (vNum b) * Rabs q'))%R;
 try ring.
rewrite Rinv_r; auto with real zarith; try rewrite Rmult_1_l.
replace (radix * pPred (vNum b) - radix)%R with
 (radix * (pPred (vNum b) - 1))%R; [ idtac | simpl in |- *; ring; ring ].
cut (1 < pPred (vNum b))%Z;
 [ intros Rlt1
 | apply Zle_lt_trans with radix;
    try apply (pPredMoreThanRadix b radix precision);
    auto with zarith ].
cut ((pPred (vNum b) - 1)%R <> 0%R);
 [ intros Rlt2
 | replace (pPred (vNum b) - 1)%R with (IZR (pPred (vNum b) - 1));
    auto with real zarith; rewrite <- Z_R_minus; simpl in |- *;
    auto ].
repeat rewrite Rinv_mult_distr; auto with real zarith.
replace
 (3%nat *
  (radix *
   (radix *
    (Rabs p' * (/ pPred (vNum b) * (/ radix * / (pPred (vNum b) - 1)))))))%R
 with
 (radix * / radix *
  (/ pPred (vNum b) * (3%nat * (radix * (Rabs p' * / (pPred (vNum b) - 1))))))%R;
 [ idtac | ring ].
rewrite Rinv_r; auto with real zarith; rewrite Rmult_1_l.
apply Rmult_lt_compat_l; auto with real.
apply Rinv_0_lt_compat; auto with real.
apply Rlt_IZRO.
apply (pPredMoreThanOne b radix precision); auto with arith.
apply Rmult_lt_reg_l with (r := (pPred (vNum b) - 1)%R); auto with real.
replace
 ((pPred (vNum b) - 1) *
  (3%nat * (radix * (Rabs (FtoRradix p') * / (pPred (vNum b) - 1)))))%R with
 (3%nat *
  (radix *
   (Rabs (FtoRradix p') * ((pPred (vNum b) - 1) * / (pPred (vNum b) - 1)))))%R;
 [ rewrite Rinv_r; auto with real zarith; try rewrite Rmult_1_r
 | ring; ring ].
apply Rplus_lt_reg_r with (Rabs (FtoRradix q'));
 repeat rewrite (Rplus_comm (Rabs (FtoRradix q'))).
replace ((pPred (vNum b) - 1) * Rabs (FtoRradix q') + Rabs (FtoRradix q'))%R
 with (pPred (vNum b) * Rabs (FtoRradix q'))%R; [ idtac | ring ].
apply Rmult_lt_reg_l with (r := (/ pPred (vNum b))%R); auto with real zarith.
rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real zarith;
 rewrite Rmult_1_l.
rewrite (fun x => Rmult_comm (/ x)); rewrite Rmult_plus_distr_r;
 repeat rewrite <- Rmult_assoc; repeat rewrite <- Rmult_assoc in H'0;
 auto.
Qed.

Theorem TwoSumNonNul :
 forall p q r pq : float,
 Fbounded b p ->
 Fbounded b q ->
 Closest b radix (p + q) pq ->
 r = (p + q - pq)%R :>R -> r <> 0%R :>R -> pq <> 0%R :>R.
intros.
Contradict H3.
rewrite H2.
apply TwoSumNul; auto with real.
Qed.

Theorem TwoSumOneNul :
 forall p q pq : float,
 Fbounded b p ->
 Fbounded b q ->
 Fbounded b pq -> Closest b radix (p + q) pq -> p = 0%R :>R -> pq = q :>R.
intros.
generalize H2.
rewrite H3.
replace (0 + q0)%R with (FtoRradix q0); [ idtac | ring ].
intro.
apply sym_eq;
 apply
  (RoundedModeProjectorIdemEq b radix precision) with (P := Closest b radix);
 auto with real float arith zarith.
apply (ClosestRoundedModeP b radix precision);
 auto with real float arith zarith.
Qed.

Theorem TwoSumOneNul2 :
 forall p q pq r : float,
 Fbounded b p ->
 Fbounded b q ->
 Fbounded b pq ->
 Closest b radix (p + q) pq ->
 p = 0%R :>R -> r = (p + q - pq)%R :>R -> r = 0%R :>R.
intros.
rewrite H4; rewrite H3.
apply Rminus_diag_eq; ring_simplify.
apply sym_eq; apply TwoSumOneNul with (p := p0); auto.
Qed.
End F2.