proposition: Theorem MKnuth : forall p q : float, Fbounded b p -> Fbounded b q -> Iminus (Iplus p q) p = (Iplus p q - p)%R :>R -> 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. rewrite IplusOl; auto with zarith. case (errorBoundedPlus b radix precision) with (p := p) (q := q) (pq := Iplus p q); auto. intros x H'2; elim H'2; intros H'3 H'4; elim H'4; intros H'5 H'6; clear H'4 H'2. unfold FtoRradix in |- *; rewrite <- H'3. apply sym_eq; apply (ClosestIdem b); auto. apply (ClosestCompatible b radix (q - Iminus (Iplus p q) p)%R ( FtoR radix x) (Iminus q (Iminus (Iplus p q) p))); auto. rewrite H'3. rewrite H'1. unfold FtoRradix in |- *; ring; ring. replace 0%R with (FtoRradix (Iminus p p)). repeat rewrite IminusPlus; apply IplusComp; repeat rewrite <- IminusPlus; auto with zarith. apply oppBounded; auto. apply oppBounded; auto. unfold FtoRradix in |- *; repeat rewrite Fopp_correct. replace (FtoR radix (Iminus (Iplus p q) (Iminus (Iplus p q) p))) with (FtoR radix p); auto. apply (ClosestIdem b); auto. apply (ClosestCompatible b radix (Iplus p q - Iminus (Iplus p q) p)%R (FtoR radix p) (Iminus (Iplus p q) (Iminus (Iplus p q) p))); auto. rewrite H'1; auto. unfold FtoRradix in |- *; ring; ring. apply IminusId; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz