proposition: Theorem MDekkerAux5 : forall p q : float, Fbounded b p -> Fbounded b q -> Iminus (Iplus (Fopp p) (Fopp q)) (Fopp p) = (Iplus (Fopp p) (Fopp q) - Fopp p)%R :>R -> Iminus (Iplus p q) p = (Iplus p q - p)%R :>R.
proof: Proof. intros p q H' H'0 H'1. rewrite <- (Fopp_Fopp (Iminus (Iplus p q) p)); auto. repeat rewrite IminusPlus; auto. rewrite IplusOp; auto. rewrite <- IminusPlus. rewrite IplusOp; auto. unfold FtoRradix in |- *; rewrite Fopp_correct. unfold FtoRradix in H'1; rewrite H'1. rewrite <- IplusOp; auto. repeat rewrite Fopp_correct. ring. Qed.
imports: Reals ZArith List PeanoNat Psatz