proposition: Theorem FulpLe : forall p : float, Fbounded b p -> (Fulp p <= Float 1 (Fexp p))%R.
proof: Proof. intros p H'; unfold Fulp, FtoRradix, FtoR, Fnormalize in |- *; simpl in |- *; rewrite Rmult_1_l. case (Z_zerop (Fnum p)); simpl in |- *; auto. intros H'0; apply (Rle_powerRZ radix (- dExp b) (Fexp p)); auto with real zarith; try apply H'. apply IZR_le; lia. intros H'0; apply Rle_powerRZ; try apply IZR_le; auto with real zarith arith. Qed.
imports: Reals ZArith List PeanoNat Psatz