proposition: Theorem IplusOl : forall p q : float, Fbounded b p -> Fbounded b q -> p = 0%R :>R -> Iplus p q = q :>R.
proof: Proof. intros p q H' H'0 H'1. rewrite IplusSym. apply (IplusOr b); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz