proposition: Theorem FvalScale : forall (b : Fbound) (p : float) (n : nat), Float (Fnum p) (Fexp p + n) = (powerRZ radix n * p)%R :>R.
proof: Proof. intros b p n; unfold FtoRradix, FtoR in |- *; simpl in |- *. rewrite powerRZ_add; auto with real zarith. ring. now apply Rgt_not_eq, IZR_lt. Qed.
imports: Reals ZArith List PeanoNat Psatz