proposition: Theorem plusExactR0 : forall p q r : float, Fbounded b p -> Fbounded b q -> Closest b radix (p + q) r -> r = 0%R :>R -> r = (p + q)%R :>R.
proof: Proof. intros p q r H' H'0 H'1 H'2. cut (r = FtoRradix (Fzero (- dExp b)) :>R); [ intros Eq1; rewrite Eq1 | rewrite H'2; apply sym_eq; unfold FtoRradix in |- *; apply FzeroisZero ]. apply plusExact1; auto. apply (ClosestCompatible b radix (p + q)%R (p + q)%R r); auto. apply FboundedFzero; auto. simpl in |- *; auto. unfold Z.min in |- *; case (Fexp p ?= Fexp q)%Z; auto with zarith; try apply H'; try apply H'0. Qed.
imports: Reals ZArith List PeanoNat Psatz