diff --git a/adlib/cert_f/nat.lp b/adlib/cert_f/nat.lp
index 57a4dc60609446e5fabcb48fcaa460be1c0aba49..29f08e2cdcf3856420f1d25a6237230ebe5ed761 100644
--- a/adlib/cert_f/nat.lp
+++ b/adlib/cert_f/nat.lp
@@ -2,15 +2,34 @@ 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 plus : Term nat ⇒ Term nat ⇒ Term nat
+set infix left 6 "+" ≔ plus
+set infix left 7 "*" ≔ times
+
+rule (succ &n) + &m → succ (&n + &m)
+ and 0 + &m → &m
+ and &n + (succ &m) → succ (&n + &m)
+ and &n + 0 → &n
+
+rule (succ &n) * &m → &n * &m + &m
+ and 0 * _ → 0
+ and &n * (succ &m) → &n * &m + &n
+ and _ * 0 → 0
+
+symbol prod_comm (x y: Term nat): Term (eq (times x y) (times y x))
+
+
+//
+// Non zero naturals
+//
+definition not_zero ≔ neq 0
+type not_zero
symbol prod_not_zero (x y: Term nat):
Term (not_zero x) ⇒ Term (not_zero y) ⇒ Term (not_zero (times x y))
-symbol prod_comm (x y: Term nat): Term (eq (times x y) (times y x))
+definition nznat ≔ psub nat not_zero
// Constructor of nznat
definition nznatc (x: Term nat) (h: Term (not_zero x)) : Term nznat ≔
diff --git a/encodings/cert_f.lp b/encodings/cert_f.lp
index 328af9d2f95e3546b031edd683961710f9af4401..72f505359fcf722d943a87804bf5ebb2f0abec28 100644
--- a/encodings/cert_f.lp
+++ b/encodings/cert_f.lp
@@ -27,7 +27,7 @@ injective symbol Term {s : Sort} : Univ s ⇒ TYPE
rule Term uProp → Univ Prop
and Term uType → Univ Type
-// [prod s1 s2 A B] encodes [Î x : (A: s1). (B x: s2)]
+// [prod s1 s2 A B] encodes [Î x : (A: s1). (B: s2)]
symbol prod {s1 s2 : Sort} (A : Univ s1) :
(Term A ⇒ Univ s2) ⇒ Univ (Rule s1 s2)
diff --git a/prelude/cert_f/booleans.lp b/prelude/cert_f/booleans.lp
index 4a01fef8d79b5a7a73837735702ec022c287953c..d01c31fae56af1cc782860a23d2feab5c7e7f5d8 100644
--- a/prelude/cert_f/booleans.lp
+++ b/prelude/cert_f/booleans.lp
@@ -4,4 +4,11 @@ definition bool ≔ uProp
definition false ≔ @prod Type Prop uProp (λ x, x)
definition true ≔ @prod Prop Prop false (λ _, false)
+definition imp (P Q: Term uProp) ≔ @prod Prop Prop P (λ_, Q)
+
definition bnot (P: Term uProp) ≔ @prod Prop Prop P (λ _, false)
+set prefix 5 "¬" ≔ bnot
+definition band (P Q: Term uProp) ≔ bnot (imp P (bnot Q))
+set infix 6 "∧" ≔ band
+definition bor (P Q: Term uProp) ≔ imp (bnot P) Q
+set infix 5 "∨" ≔ bor
diff --git a/prelude/cert_f/equality_props.lp b/prelude/cert_f/equality_props.lp
new file mode 100644
index 0000000000000000000000000000000000000000..33ba4c8d6a86588f536b6fa5161243cc3d269396
--- /dev/null
+++ b/prelude/cert_f/equality_props.lp
@@ -0,0 +1,22 @@
+require open encodings.cert_f
+prelude.cert_f.booleans
+prelude.cert_f.equalities
+prelude.cert_f.if_def
+
+rule if true &t _ → &t
+ and if false _ &f → &f
+
+theorem if_same T (b: Term uProp) (x: Term T):
+ Term (eq (if b x x) x)
+proof
+assume T b x
+simpl
+admit // Needs case disjunciton on boolean
+
+symbol reflexivity_of_equal T (x: Term T) : Term (eq x x)
+
+symbol transitivity_of_equal T (x y z: Term T) :
+ Term ((eq x y) ∧ (eq y z)) ⇒ Term (eq x z)
+
+symbol symmetry_of_equal T (x y: Term T):
+ Term (eq x y) ⇒ Term (eq y x)
diff --git a/prelude/cert_f/if_def.lp b/prelude/cert_f/if_def.lp
index a4276a8daafab0e6cf37b799dc3355c5e4de0f33..37aaea99e3205893e3df8c191309b2761fe8c819 100644
--- a/prelude/cert_f/if_def.lp
+++ b/prelude/cert_f/if_def.lp
@@ -1,6 +1,3 @@
require open encodings.cert_f prelude.cert_f.booleans
symbol if {T: Term uType} : Term uProp ⇒ Term T ⇒ Term T ⇒ Term T
-
-rule if true &t _ → &t
- and if false _ &f → &f
diff --git a/sandbox/cert_f/even.lp b/sandbox/cert_f/even.lp
new file mode 100644
index 0000000000000000000000000000000000000000..ff5c8073a5eb5156677e3bf2c1e6d2bdeeb06988
--- /dev/null
+++ b/sandbox/cert_f/even.lp
@@ -0,0 +1,25 @@
+require open encodings.cert_f
+prelude.cert_f.equalities
+prelude.cert_f.naturalnumbers
+adlib.cert_f.nat
+
+symbol mod2: Term nat ⇒ Term nat
+rule mod2 (&n + 2) → mod2 &n
+ and mod2 ( _ + 1) → 1
+ and mod2 0 → 0
+
+definition is_even (n: Term nat) ≔ eq (mod2 n) 0
+
+definition Even ≔ psub nat is_even
+
+definition evenify (n: Term nat) (h: Term (is_even n)) : Term Even ≔
+ pair is_even n h
+
+definition even_to_nat ≔ fst is_even
+
+theorem twice_even_even (n: Term Even):
+ Term (is_even (2 * even_to_nat n))
+proof
+assume n
+simpl
+qed
diff --git a/sandbox/cert_f/rat.lp b/sandbox/cert_f/rat.lp
index 0beee5913ddbc51a72973283345509d8787aa278..82c3cab3d600bb5f8947abe1583000e588ff5304 100644
--- a/sandbox/cert_f/rat.lp
+++ b/sandbox/cert_f/rat.lp
@@ -7,6 +7,7 @@ constant symbol rat : Univ Type
constant symbol zero : Term rat
symbol frac : Term nat ⇒ Term N.nznat ⇒ Term rat
+set infix 8 "/" ≔ frac
symbol times : @Term Type rat ⇒ @Term Type rat ⇒ @Term Type rat
@@ -22,12 +23,28 @@ rule times (frac &a &b) (frac &c &d) →
(snd N.not_zero &d)))
symbol rateq : Term rat ⇒ Term rat ⇒ Univ Prop
-rule rateq (frac &a &b) (frac &c &d) →
- eq (N.times &a (fst N.not_zero &d)) (N.times (fst N.not_zero &b) &c)
+rule rateq (&a / &b) (&c / &d) →
+ let nzval x ≔ fst N.not_zero x in
+ eq (N.times &a (nzval &d)) (N.times (nzval &b) &c)
definition onz : Term N.nznat ≔ N.nznatc 1 N.one_not_zero
-theorem right_cancellation (a: Term nat) (b: Term N.nznat):
- Term (rateq (times (frac a b) (frac (fst N.not_zero b) onz)) (frac a onz))
+theorem rrefl (a: Term nat) (b: Term N.nznat):
+ Term (rateq (a / b) (a / b))
proof
-admit
+assume a b
+apply N.prod_comm a (fst N.not_zero b)
+qed
+
+theorem one_neutral (a: Term nat) (b: Term N.nznat):
+ Term (rateq (times (a / b) (1 / onz)) (1 / onz))
+proof
+assume a b
+refine N.prod_comm ?p1[a,b] ?p2[a,b]
+qed
+// theorem right_cancellation (a: Term nat) (b: Term N.nznat):
+// Term (rateq (times (a / b) ((fst N.not_zero b) / onz)) (a / onz))
+// proof
+// assume a b
+// refine Term
+// qed