proposition: Theorem MKnuth7 : forall p q : float, (Rabs 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. cut (0 < q)%R; [ intros Rlt1 | apply Rle_lt_trans with (2 := H'); auto with real ]. case (Rle_or_lt 0 p); intros Rle1; [ Casec Rle1; intros Rle1 | idtac ]. apply MKnuth5; auto. rewrite <- (Rabs_right p); auto with real; apply Rle_ge; apply Rlt_le; auto. apply MKnuth6; auto. apply IplusCorrectEq with (pq := q); auto; rewrite <- Rle1; ring. case (Rle_or_lt q (radix * - p)); intros Rle2. apply MKnuth3; auto. apply Rlt_le; auto. rewrite <- (Rabs_left1 p); auto; apply Rlt_le; auto. apply MKnuth4; auto. replace 0%R with (-0)%R; [ auto with real | ring ]. apply Rabs_pos. Qed.
imports: Reals ZArith List PeanoNat Psatz