diff --git a/adlib/cert_f/nat.lp b/adlib/cert_f/nat.lp
new file mode 100644
index 0000000000000000000000000000000000000000..53cd195e52be496a5d31dc67aba20a6742771e22
--- /dev/null
+++ b/adlib/cert_f/nat.lp
@@ -0,0 +1,15 @@
+require open encodings.cert_f prelude.cert_f.booleans
+prelude.cert_f.equalities prelude.cert_f.notequal
+prelude.cert_f.naturalnumbers
+
+definition not_zero ≔ neq 0
+definition nznat ≔ psub nat not_zero
+
+symbol times : Term nat ⇒ Term nat ⇒ Term nat
+
+symbol prod_not_zero (x y: Term nat):
+  Term (not_zero x) ⇒ Term (not_zero y) ⇒ Term (not_zero (times x y))
+
+// Constructor of nznat
+definition nznatc (x: Term nat) (h: Term (not_zero x)) ≔
+  pair not_zero x h
diff --git a/sandbox/cert_f/rat.lp b/sandbox/cert_f/rat.lp
new file mode 100644
index 0000000000000000000000000000000000000000..c48a3224e17d0979ef9dcbf5d712c91c58061a7a
--- /dev/null
+++ b/sandbox/cert_f/rat.lp
@@ -0,0 +1,20 @@
+require open encodings.cert_f prelude.cert_f.booleans
+prelude.cert_f.equalities prelude.cert_f.notequal
+prelude.cert_f.naturalnumbers prelude.cert_f.int
+require adlib.cert_f.nat as N
+
+constant symbol rat : Univ Type
+constant symbol zero : Term rat
+
+symbol frac : Term nat ⇒ Term N.nznat ⇒ Term rat
+
+symbol times : @Term Type rat ⇒ @Term Type rat ⇒ @Term Type rat
+
+rule times (frac &a &b) (frac &c &d) →
+  let bv ≔ @fst nat N.not_zero &b in
+  let bpr ≔ @snd nat N.not_zero &b in
+  let dv ≔ @fst nat N.not_zero &d in
+  let dpr ≔ @snd nat N.not_zero &d in
+  frac
+   (N.times &a &c)
+   (N.nznatc (N.times bv dv) (N.prod_not_zero bv dv bpr dpr))