diff --git a/lib/pulse/core/PulseCore.FractionalPermission.fst b/lib/pulse/core/PulseCore.FractionalPermission.fst
index 3d7028680..3e54acbed 100644
--- a/lib/pulse/core/PulseCore.FractionalPermission.fst
+++ b/lib/pulse/core/PulseCore.FractionalPermission.fst
@@ -28,4 +28,4 @@ include FStar.Real
 /// when writing something like `p1+p2`, but every library does in fact limit
 /// permissions to 1.0R.
 [@@ erasable]
-type perm : Type0 = r:real { r >. zero }
+type perm : Type0 = r:real { r >. 0.0R }