proposition: Theorem IminusId : forall p q : float, Fbounded b p -> Fbounded b q -> p = q :>R -> Iminus p q = 0%R :>R.
proof: Proof. intros p q H' H'0 H'1. cut (Closest b radix (p - q) (Iminus p q)); auto. replace (p - q)%R with 0%R; [ idtac | rewrite <- H'1; ring ]. replace 0%R with (FtoRradix (Fzero (- dExp b))). intros H'2; apply sym_eq. unfold FtoRradix in |- *; apply (ClosestIdem b radix); auto. apply FboundedFzero; auto. unfold Fzero, FtoRradix, FtoR in |- *; simpl in |- *; ring. apply IminusCorrect; easy. Qed.
imports: Reals ZArith List PeanoNat Psatz