proposition: Theorem MDekkerAux2 : forall p q : float, Iplus p q = (p + q)%R :>R -> Fbounded b p -> Fbounded b q -> Iminus (Iplus p q) p = (Iplus p q - p)%R :>R.
proof: Proof. intros p q H' H'0 H'1. cut (Closest b radix (Iplus p q - p) (Iminus (Iplus p q) p)); auto. repeat rewrite H'. replace (p + q - p)%R with (FtoRradix q); [ idtac | ring ]. intros H'2. apply sym_eq; apply (ClosestIdem b radix); auto. apply IminusCorrect; auto. apply IplusBounded; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz