proposition: Theorem LeFulpPos : forall x y : float, Fbounded b x -> Fbounded b y -> (0 <= x)%R -> (x <= y)%R -> (Fulp x <= Fulp y)%R.
proof: Proof. intros x y Hx Hy H1 H2; unfold Fulp in |- *. apply Rle_powerRZ; try apply IZR_le; auto with real zarith. apply Fcanonic_Rle_Zle with radix b precision; auto with zarith arith. apply FnormalizeCanonic; auto with zarith arith. apply FnormalizeCanonic; auto with zarith arith. repeat rewrite FnormalizeCorrect; auto with zarith arith real. repeat rewrite Rabs_right; auto with zarith arith real. apply Rge_trans with (FtoRradix x); auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz