proposition: Theorem MDekkerAux3 : forall p q : float, Fbounded b (Fplus radix p q) -> 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. apply MDekkerAux2; auto. unfold FtoRradix in |- *; rewrite <- Fplus_correct; auto. apply sym_eq; apply (ClosestIdem b radix); auto. rewrite Fplus_correct; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz