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