proposition: Theorem TwoSumProp: forall (a b x y:float), (Fbounded bo a) -> (Closest bo radix (a+b)%R x) -> (FtoRradix y=a+b-x)%R -> (Rabs y <= Rabs b)%R.
proof: Proof. intros. elim H0; fold FtoRradix; intros. rewrite <- (Rabs_Ropp y); rewrite <- (Rabs_Ropp b). replace (-y)%R with (x-(a+b))%R;[idtac|rewrite H1; ring]. replace (-b)%R with (a-(a+b))%R;[idtac|ring]. apply H3; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz