proposition: Theorem MKnuth3 : forall p q : float, (0 <= q)%R -> (q <= radix * - p)%R -> (- p <= q)%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 H'2 H'3. apply MKnuth; auto. cut (FtoRradix (Iplus p q) = (p + q)%R :>R); [ intros Eq1 | idtac ]. apply IminusCorrectEq with (pq := q); auto. rewrite Eq1; ring. rewrite Eq1; ring. apply IplusCorrectEq with (pq := Fminus radix q (Fopp p)); auto. apply Sterbenz; auto with zarith. apply oppBounded; auto. 2: repeat rewrite (Fopp_correct radix); auto. 2: rewrite (Fminus_correct radix); repeat rewrite (Fopp_correct radix); unfold FtoRradix in |- *; auto; ring; ring. 2: rewrite (Fminus_correct radix); repeat rewrite (Fopp_correct radix); unfold FtoRradix in |- *; auto; ring; ring. apply Rle_trans with (2 := H'1). apply Rmult_le_reg_l with (r := IZR radix); auto with real. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real arith; rewrite Rmult_1_l. rewrite (Fopp_correct radix). apply Rle_trans with (1 := H'1); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz