proposition: Theorem Knuth : forall p q : float, 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; case (Rle_or_lt (Rabs q) (Rabs p)); intros Rle1. apply MKnuth2; auto. case (Rle_or_lt 0 q); intros Rle2. apply MKnuth7; auto. rewrite <- (Rabs_right q); auto with real; apply Rle_ge; apply Rlt_le; auto. rewrite MKnuthOpp. rewrite (Fopp_correct radix). replace (p + q - Iplus p q)%R with (- (Fopp p + Fopp q - Iplus (Fopp p) (Fopp q)))%R. cut (forall x y : R, x = y -> (- x)%R = (- y)%R); [ intros tmp; apply tmp; clear tmp | intros x y tmp; rewrite tmp; auto ]. apply MKnuth7; auto with zarith. repeat rewrite (Fopp_correct radix); auto. rewrite <- (Rabs_left1 (FtoR radix q)); try apply Rlt_le; auto. rewrite Rabs_Ropp; auto. apply oppBounded; auto. apply oppBounded; auto. rewrite <- IplusOp; repeat rewrite (Fopp_correct radix); unfold FtoRradix in |- *; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz