proposition: Theorem MDekkerAux4 : forall p q : float, Fbounded b (Fminus radix (Iplus p q) p) -> 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. unfold FtoRradix in |- *; rewrite <- Fminus_correct; auto. apply sym_eq; apply (ClosestIdem b radix); auto. rewrite Fminus_correct; auto. apply IminusCorrect; auto. repeat (try apply IplusBounded; try apply IminusBounded; auto); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz