proposition: Theorem plusExact2 : forall p q r : float, Fcanonic radix b p -> Fbounded b q -> Closest b radix (p + q) r -> (Fexp r < Z.pred (Fexp p))%Z -> r = (p + q)%R :>R.
proof: Proof. intros p q r H' H'0 H'1 H'2. case (Rle_or_lt 0 p); intros Rl1. apply plusExact2Aux; auto. replace (p + q)%R with (- (Fopp p + Fopp q))%R. rewrite <- (plusExact2Aux (Fopp p) (Fopp q) (Fopp r)); auto. unfold FtoRradix in |- *; rewrite Fopp_correct; ring. unfold FtoRradix in |- *; rewrite Fopp_correct. apply Rlt_le; replace 0%R with (-0)%R; auto with real. apply FcanonicFopp; auto with arith. apply oppBounded; auto. replace (Fopp p + Fopp q)%R with (- (p + q))%R. apply ClosestOpp; auto. unfold FtoRradix in |- *; repeat rewrite Fopp_correct; ring. unfold FtoRradix in |- *; repeat rewrite Fopp_correct; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz