proposition: Theorem MKnuth6 : forall p q : float, Iplus p q = (p + q)%R :>R -> Fbounded b p -> Fbounded b q -> Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p))) (Iminus q (Iminus (Iplus p q) p)) = (p + q - Iplus p q)%R :>R.
proof: Proof. intros p q H' H'0 H'1. apply MKnuth; auto. apply IminusCorrectEq with (pq := q); auto. rewrite H'; ring. rewrite H'; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz