proposition: Theorem IplusOr : forall p q : float, Fbounded b p -> Fbounded b q -> q = 0%R :>R -> Iplus p q = p :>R.
proof: Proof. intros p q H' H'0 H'1. cut (Closest b radix (p + q) (Iplus p q)); auto. rewrite H'1. rewrite Rplus_0_r. intros H'2; apply sym_eq. unfold FtoRradix in |- *; apply (ClosestIdem b radix); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz