proposition: Theorem FBoundedScale : forall (b : Fbound) (p : float) (n : nat), Fbounded b p -> Fbounded b (Float (Fnum p) (Fexp p + n)).
proof: Proof. intros b p n H'; repeat split; simpl in |- *; auto; try apply H'. apply Z.le_trans with (Fexp p); try apply H'. lia. Qed.
imports: Reals ZArith List PeanoNat Psatz