FractionalPermission: use a literal 0.0R

This enables simplification rules (from
FStarLang/FStar#3305) to kick in, and
potentially significantly reduce the number of queries we send to the
SMT. For instance, for DPE.fst:

Before (595 total queries):
	Verified module: DPE
	All verification conditions discharged successfully
	ramon: end                  Thu May 23 10:25:28 2024
	ramon: root.execname        fstar.exe
	ramon: root.utime           12.940s
	ramon: root.stime           0.160s
	ramon: group.total          139.763s
	ramon: group.utime          139.459s
	ramon: group.stime          0.304s
	ramon: group.mempeak        2181MiB
	ramon: group.pidpeak        4
	ramon: status               exited
	ramon: exitcode             0
	ramon: walltime             139.706s
	ramon: loadavg              1.00

After (448 total queries):
	Verified module: DPE
	All verification conditions discharged successfully
	ramon: end                  Thu May 23 10:31:30 2024
	ramon: root.execname        fstar.exe
	ramon: root.utime           12.550s
	ramon: root.stime           0.130s
	ramon: group.total          110.062s
	ramon: group.utime          109.754s
	ramon: group.stime          0.308s
	ramon: group.mempeak        2094MiB
	ramon: group.pidpeak        4
	ramon: status               exited
	ramon: exitcode             0
	ramon: walltime             110.032s
	ramon: loadavg              1.00

So a 21% speedup. There are more optimizations we could do. The F*
rules in that PR only check for 1.0/0.5/0.0 and decide comparisons
between them.

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 }