diff --git a/Bool.lp b/Bool.lp
index 8cac791..1c9bd24 100644
--- a/Bool.lp
+++ b/Bool.lp
@@ -104,6 +104,26 @@ begin
   { simplify; assume h0 h1; refine h1 }
 end;
 
+opaque symbol notK b : π (not (not b) = b) ≔
+begin
+  induction
+  { reflexivity }
+  { reflexivity }
+end;
+
+opaque symbol not_inj [b c] : π (not b = not c) → π (b = c) ≔
+begin
+  induction
+  { induction
+    { assume h; reflexivity }
+    { assume h; apply ⊥ₑ (false≠true h) }
+  }
+  { induction
+    { assume h; apply ⊥ₑ (true≠false h) }
+    { assume h; reflexivity }
+  }
+end;
+
 // or
 
 symbol or : 𝔹 → 𝔹 → 𝔹;
@@ -129,6 +149,49 @@ begin
     {reflexivity}
 end;
 
+// imp
+
+symbol imp (b c : 𝔹) : 𝔹 ≔ not b or c;
+
+notation imp infix left 20;
+
+opaque symbol ⇒_istrue [p q : 𝔹] : π(p imp q) → π(p ⇒ q) ≔
+begin
+  induction
+  { induction
+    { assume h1; refine (λ x, x) }
+    { assume h1 h2; refine h1 }
+  }
+  {
+    induction
+    { assume h1 h2; apply h1 }
+    { assume h1; refine (λ x, x) }
+   }
+end;
+
+opaque symbol istrue_imp [p q : 𝔹] : π(p ⇒ q) → π(p imp q) ≔
+begin
+  induction
+  { induction
+    { assume h; apply ⊤ᵢ }
+    { assume h; apply h ⊤ᵢ }
+  }
+  { induction
+    { assume h; apply ⊤ᵢ }
+    { assume h; apply ⊤ᵢ }
+  }
+end;
+
+opaque symbol impᵢ [p q : 𝔹] : (π p → π q) → π (p imp q) ≔
+begin
+  assume p q h; apply @istrue_imp p q h;
+end;
+
+opaque symbol impₑ [p q : 𝔹] : π (p imp q) → π p → π q ≔
+begin
+  assume p q h; refine @⇒_istrue p q h;
+end;
+
 opaque symbol ∨_istrue [p q : 𝔹] : π(p or q) → π(p ∨ q) ≔
 begin
   induction
@@ -226,9 +289,86 @@ begin
   { assume q i; apply ⊥ₑ i; }
 end;
 
+// xorb
+
+symbol xorb : 𝔹 → 𝔹 → 𝔹;
+
+notation xorb infix left 22;
+
+rule false xorb $b ↪ $b
+with true xorb $b ↪ not $b;
+
+opaque symbol xorbᵢ₁ [p q : 𝔹] : π p → π (not q) → π (p xorb q) ≔
+begin
+  induction
+  { assume q h i; apply i }
+  { assume q h i; apply ⊥ₑ h }
+end;
+
+opaque symbol xorbᵢ₂ [p q : 𝔹] : π (not p) → π q → π (p xorb q) ≔
+begin
+  induction
+  { assume q h i; apply ⊥ₑ h }
+  { assume q h i; apply i }
+end;
+
+opaque symbol xorbₑ [p q : 𝔹] (r : 𝔹) :
+  π (p xorb q) → (π p → π (not q) → π r) → (π (not p) → π q → π r) → π r ≔
+begin
+  induction
+  { assume q r h h1 h2; apply h1 ⊤ᵢ h }
+  { assume q r h h1 h2; apply h2 ⊤ᵢ h }
+end;
+
 // if-then-else
 
 symbol if : 𝔹 → Π [a], τ a → τ a → τ a;
 
 rule if true  $x _ ↪ $x
 with if false _ $y ↪ $y;
+
+opaque symbol if_true [a] (x y : τ a) : π (if true x y = x) ≔
+begin reflexivity end;
+
+opaque symbol if_false [a] (x y : τ a) : π (if false x y = y) ≔
+begin reflexivity end;
+
+opaque symbol if_same b [a] (x : τ a) : π (if b x x = x) ≔
+begin
+  assume b a x;
+  refine ∨ₑ (case_𝔹 b) _ _
+    { assume h; rewrite h; reflexivity }
+    { assume h; rewrite h; reflexivity }
+end;
+
+opaque symbol if_id b : π (if b true false = b) ≔
+begin
+  induction
+  { reflexivity }
+  { reflexivity }
+end;
+
+opaque symbol if_not b [a] (x y : τ a) : π (if (not b) x y = if b y x) ≔
+begin
+  assume b a x y;
+  refine ∨ₑ (case_𝔹 b) _ _
+    { assume h; rewrite h; reflexivity }
+    { assume h; rewrite h; reflexivity }
+end;
+
+opaque symbol if_istrue [b : 𝔹] [a] (x y : τ a) : π b → π (if b x y = x) ≔
+begin
+  assume b a x y h;
+  refine ∨ₑ (case_𝔹 b) _ _
+    { assume h1; rewrite h1; reflexivity }
+    { assume h1; apply ⊥ₑ (false=¬istrue h1 h) }
+end;
+
+opaque symbol if_isfalse [b : 𝔹] [a] (x y : τ a) : π (not b) → π (if b x y = y) ≔
+begin
+  assume b a x y h;
+  refine ∨ₑ (case_𝔹 b) _ _
+    { assume h1; apply ⊥ₑ (istrue_not h (true=istrue h1)) }
+    { assume h1; rewrite h1; reflexivity }
+end;
+
diff --git a/CHANGES.md b/CHANGES.md
index 975d7cf..a090b18 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -11,6 +11,16 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 - Univ: universe levels for Set and Prop
 - Quotient: quotient types
 - NaryFun: n-ary functions and relations
+- Bool: imp, xorb, not_inj and theorems on if-then-else
+- Epsilon: εₑ
+- List: foldl, foldr, All, mergesort and its correctness
+- Nat: parity, div2, shifts, bitwise operations and strong induction
+- Pos: theorems on multiplication
+- Prod: theorems on the Cartesian product
+- Coprod: the co-Cartesian product (disjoint sum)
+- Subset: subset types
+- DepProd: dependent products and transport
+- Z: theorems on multiplication, power and comparison
 
 ### Changed
 
diff --git a/Coprod.lp b/Coprod.lp
new file mode 100644
index 0000000..a2ad23f
--- /dev/null
+++ b/Coprod.lp
@@ -0,0 +1,144 @@
+// Co-Cartesian product (disjoint sum)
+
+require open Stdlib.FOL Stdlib.Eq;
+
+(a: Set) (b: Set) inductive Sum: TYPE ≔
+| inl: τ a → Sum a b
+| inr: τ b → Sum a b;
+
+constant symbol sum : Set → Set → Set;
+
+rule τ (sum $a $b) ↪ Sum $a $b;
+
+// Universal property: a map out of a sum is given by case analysis
+
+symbol sum_case [a b c] : τ (sum a b) → (τ a → τ c) → (τ b → τ c) → τ c;
+
+rule sum_case (inl $x) $f _ ↪ $f $x
+with sum_case (inr $y) _ $g ↪ $g $y;
+
+opaque symbol sum_case_uniq [a b c] (h: τ (sum a b) → τ c) (s: τ (sum a b)) :
+  π (sum_case s (λ x, h (inl x)) (λ y, h (inr y)) = h s) ≔
+begin
+  assume a b c h; induction { reflexivity } { reflexivity }
+end;
+
+opaque symbol η_sum [a b] (s: τ (sum a b)) :
+  π (sum_case s (λ x, inl x) (λ y, inr y) = s) ≔
+begin
+  assume a b; induction { reflexivity } { reflexivity }
+end;
+
+// non confusion of constructors
+
+symbol is_inl [a b] : τ (sum a b) → Prop;
+
+rule is_inl (inl _) ↪ ⊤
+with is_inl (inr _) ↪ ⊥;
+
+opaque symbol inr≠inl [a b] (x: τ a) (y: τ b) : π (@inr a b y ≠ inl x) ≔
+begin assume a b x y h; refine ind_eq h (λ s, is_inl s) ⊤ᵢ end;
+
+opaque symbol inl≠inr [a b] (x: τ a) (y: τ b) : π (@inl a b x ≠ inr y) ≔
+begin assume a b x y h; apply inr≠inl x y; symmetry; apply h end;
+
+symbol outl [a b] (s: τ (sum a b)) : τ a ≔ sum_case s (λ x, x) (λ _, el a);
+symbol outr [a b] (s: τ (sum a b)) : τ b ≔ sum_case s (λ _, el b) (λ y, y);
+
+opaque symbol inl_inj [a b] (x x': τ a) : π (@inl a b x = inl x') → π (x = x') ≔
+begin assume a b x x' h; refine feq (λ s, @outl a b s) h end;
+
+opaque symbol inr_inj [a b] (y y': τ b) : π (@inr a b y = inr y') → π (y = y') ≔
+begin assume a b y y' h; refine feq (λ s, @outr a b s) h end;
+
+// induction principle with equalities
+
+opaque symbol case_Sum [a b] (s: τ (sum a b)) :
+  π ((`∃ x, s = inl x) ∨ (`∃ y, s = inr y)) ≔
+begin
+  assume a b; induction
+  { assume x; apply ∨ᵢ₁; apply ∃ᵢ x; reflexivity }
+  { assume y; apply ∨ᵢ₂; apply ∃ᵢ y; reflexivity }
+end;
+
+opaque symbol ind_Sum_eq [a b] (p: τ (sum a b) → Prop) (s: τ (sum a b)) :
+  (Π x, π (s = inl x) → π (p s)) → (Π y, π (s = inr y) → π (p s)) → π (p s) ≔
+begin
+  assume a b p s hl hr; refine ∨ₑ (case_Sum s) (λ h, ∃ₑ h hl) (λ h, ∃ₑ h hr)
+end;
+
+symbol map_sum [a b c d] (f: τ a → τ c) (g: τ b → τ d) (s: τ (sum a b))
+  : τ (sum c d) ≔ sum_case s (λ x, inl (f x)) (λ y, inr (g y));
+
+opaque symbol map_sum_id [a b] (s: τ (sum a b)) :
+  π (map_sum (λ u, u) (λ v, v) s = s) ≔
+begin assume a b s; refine η_sum s end;
+
+opaque symbol map_sum_comp [a b c d e f]
+  (g: τ c → τ e) (g': τ d → τ f) (h: τ a → τ c) (h': τ b → τ d) (s: τ (sum a b)) :
+  π (map_sum g g' (map_sum h h' s) = map_sum (λ u, g (h u)) (λ v, g' (h' v)) s) ≔
+begin
+  assume a b c d e f g g' h h';
+  induction { reflexivity } { reflexivity }
+end;
+
+symbol swap_sum [a b] (s: τ (sum a b)) : τ (sum b a) ≔
+  sum_case s (λ x, inr x) (λ y, inl y);
+
+opaque symbol swap_sum_invol [a b] (s: τ (sum a b)) :
+  π (swap_sum (swap_sum s) = s) ≔
+begin
+  assume a b; induction { reflexivity } { reflexivity }
+end;
+
+// currying
+
+symbol sum_curry₁ [a b c] (h: τ (sum a b) → τ c) (x: τ a) : τ c ≔ h (inl x);
+symbol sum_curry₂ [a b c] (h: τ (sum a b) → τ c) (y: τ b) : τ c ≔ h (inr y);
+
+symbol sum_uncurry [a b c] (f: τ a → τ c) (g: τ b → τ c) (s: τ (sum a b)) : τ c ≔
+  sum_case s f g;
+
+opaque symbol sum_uncurry_curry [a b c] (h: τ (sum a b) → τ c) (s: τ (sum a b)) :
+  π (sum_uncurry (sum_curry₁ h) (sum_curry₂ h) s = h s) ≔
+begin
+  assume a b c h; induction { reflexivity } { reflexivity }
+end;
+
+opaque symbol sum_curry_uncurry₁ [a b c] (f: τ a → τ c) (g: τ b → τ c) (x: τ a) :
+  π (sum_curry₁ (sum_uncurry f g) x = f x) ≔
+begin reflexivity end;
+
+opaque symbol sum_curry_uncurry₂ [a b c] (f: τ a → τ c) (g: τ b → τ c) (y: τ b) :
+  π (sum_curry₂ (sum_uncurry f g) y = g y) ≔
+begin reflexivity end;
+
+// Relation between the product and the coproduct
+
+require open Stdlib.Prod;
+
+symbol dist_× [a b c] (x: τ (a × sum b c)) : τ (sum (a × b) (a × c)) ≔
+  sum_case (x ₂) (λ y, inl ((x ₁) ‚ y)) (λ z, inr ((x ₁) ‚ z));
+
+symbol undist_× [a b c] (s: τ (sum (a × b) (a × c))) : τ (a × sum b c) ≔
+  sum_case s (λ u, (u ₁) ‚ inl (u ₂)) (λ v, (v ₁) ‚ inr (v ₂));
+
+opaque symbol undist_dist_‚ [a b c] (u: τ a) (s: τ (sum b c)) :
+  π (undist_× (dist_× (u ‚ s)) = u ‚ s) ≔
+begin
+  assume a b c u; induction { reflexivity } { reflexivity }
+end;
+
+opaque symbol undist_dist_× [a b c] (x: τ (a × sum b c)) :
+  π (undist_× (dist_× x) = x) ≔
+begin
+  assume a b c x; rewrite prodExt x; refine undist_dist_‚ (x ₁) (x ₂)
+end;
+
+opaque symbol dist_undist_× [a b c] (s: τ (sum (a × b) (a × c))) :
+  π (dist_× (undist_× s) = s) ≔
+begin
+  assume a b c; induction
+  { assume u; symmetry; refine feq inl (prodExt u) }
+  { assume v; symmetry; refine feq inr (prodExt v) }
+end;
diff --git a/DepProd.lp b/DepProd.lp
new file mode 100644
index 0000000..b32b265
--- /dev/null
+++ b/DepProd.lp
@@ -0,0 +1,38 @@
+// Dependent product: a dependent pair of an element and an element in Set
+
+require open Stdlib.Eq;
+
+[a: Set] (p: τ a → Set) inductive DProd : TYPE ≔
+  dpair (x: τ a) : τ (p x) → DProd p;
+
+constant symbol dprod [a: Set] : (τ a → Set) → Set;
+
+rule τ (@dprod $a $p) ↪ @DProd $a $p;
+
+symbol proj₁ [a] [p] (e: @DProd a p) : τ a;
+
+rule proj₁ (dpair $x _) ↪ $x;
+
+symbol proj₂ [a] [p] (e: @DProd a p) : τ (p (proj₁ e));
+
+rule proj₂ (dpair _ $u) ↪ $u;
+
+opaque symbol η_dprod [a] [p] (e: @DProd a p) :
+  π (dpair (proj₁ e) (proj₂ e) = e) ≔
+begin assume a p; induction; assume x u; reflexivity end;
+
+opaque symbol eq_proj₁ [a] [p] (x y: @DProd a p) :
+  π (x = y) → π (proj₁ x = proj₁ y) ≔
+begin assume a p x y h; refine feq (λ e, proj₁ e) h end;
+
+opaque symbol eq_dpair_refl [a] [p] (x: τ a) (u v: τ (p x)) :
+  π (u = v) → π (@dpair a p x u = dpair x v) ≔
+begin
+  assume a p x u v h; refine feq (λ w, @dpair a p x w) h
+end;
+
+symbol transport [a] (p: τ a → Set) [x y: τ a] : π (x = y) → τ (p x) → τ (p y);
+rule transport _ (eq_refl _) $u ↪ $u;
+
+symbol eq_dpair [a] [p] (x y: τ a) (u: τ (p x)) (v: τ (p y)) (h: π (x = y)) :
+  π (transport p h u = v) → π (@dpair a p x u = dpair y v);
diff --git a/Epsilon.lp b/Epsilon.lp
index fcb100e..462536d 100644
--- a/Epsilon.lp
+++ b/Epsilon.lp
@@ -2,3 +2,8 @@ require open Stdlib.FOL;
 
 symbol ε [a:Set] : (τ a → Prop) → τ a;
 symbol εᵢ [a:Set] (p:τ a → Prop) : π (∃ p) → π (p (ε p));
+
+opaque symbol εₑ [a:Set] (p:τ a → Prop) : π (p (ε p)) → π (`∃ x, p x) ≔
+begin
+  assume a p h; refine ∃ᵢ (ε p) h
+end;
diff --git a/ExtraRules.lp b/ExtraRules.lp
index ce9aa22..0259466 100644
--- a/ExtraRules.lp
+++ b/ExtraRules.lp
@@ -39,6 +39,7 @@ rule P.add $x P.H ↪ P.succ $x
 with P.add P.H $y ↪ P.succ $y;
 rule P.add_carry $x P.H ↪ P.add $x (P.O P.H)
 with P.add_carry P.H $y ↪ P.add (P.O P.H) $y;
+rule P.mul $x P.H ↪ $x;
 
 // Z
 
diff --git a/List.lp b/List.lp
index 2b8a7d3..8396b8d 100644
--- a/List.lp
+++ b/List.lp
@@ -1903,20 +1903,264 @@ begin
     refine eq_refl (x ⸬ l) }
 end;
 
-// sumn
+// foldr
+
+symbol foldr [a b] : (τ b → τ a → τ a) → τ a → 𝕃 b → τ a;
+
+rule foldr _ $acc □ ↪ $acc
+with foldr $op $acc ($h ⸬ $tl) ↪ $op $h (foldr $op $acc $tl);
+
+// foldl
+
+symbol foldl [a b] : (τ a → τ b → τ a) → τ a → 𝕃 b → τ a;
 
-symbol sumn : 𝕃 nat → ℕ;
+rule foldl _ $acc □ ↪ $acc
+with foldl $op $acc ($h ⸬ $tl) ↪ foldl $op ($op $acc $h) $tl;
 
-rule sumn □ ↪ 0
-with sumn ($x ⸬ $l) ↪ $x + sumn $l;
+assert ⊢ foldl (+) 0 (3 ⸬ 2 ⸬ 1 ⸬ □) ≡ foldr (+) 0 (3 ⸬ 2 ⸬ 1 ⸬ □);
+
+// sumn
+
+symbol sumn (l : 𝕃 nat) : ℕ ≔ foldr (+) 0 l;
 
 assert ⊢ sumn (3 ⸬ 2 ⸬ 1 ⸬ □) ≡ 6;
 
 // prodn
 
-symbol prodn : 𝕃 nat → ℕ;
-
-rule prodn □ ↪ 1
-with prodn ($x ⸬ $l) ↪ $x * prodn $l;
+symbol prodn (l : 𝕃 nat) : ℕ ≔ foldr (*) 1 l;
 
 assert ⊢ prodn (3 ⸬ 2 ⸬ 1 ⸬ □) ≡ 3 !;
+
+// Sorting algorithm Merge Sort
+
+symbol split [a: Set] (l : τ (list a)) : τ (list a × list a);
+
+rule split □ ↪ □ ‚ □
+with split ($x ⸬ □) ↪ ($x ⸬ □) ‚ □
+with split ($x ⸬ $y ⸬ $l) ↪
+    let res ≔ split $l in ($x ⸬ (res ₁)) ‚ ($y ⸬ (res ₂));
+
+// merge and mergesort are parametrised by a boolean ordering on the elements
+
+symbol merge [a] : (τ a → τ a → 𝔹) → 𝕃 a → 𝕃 a → 𝕃 a;
+
+rule merge _ □ $l2 ↪ $l2
+with merge _ $l1 □ ↪ $l1
+with merge $≤ ($a1 ⸬ $l1') ($a2 ⸬ $l2') ↪
+    if ($≤ $a1 $a2)
+        ($a1 ⸬ merge $≤ $l1' ($a2 ⸬ $l2'))
+        ($a2 ⸬ merge $≤ ($a1 ⸬ $l1') $l2');
+
+symbol mergesort [a] : (τ a → τ a → 𝔹) → 𝕃 a → 𝕃 a;
+
+rule mergesort _ □ ↪ □
+with mergesort _ ($x ⸬ □) ↪ $x ⸬ □
+with mergesort $≤ ($x ⸬ $y ⸬ $l) ↪
+  let s ≔ split ($x ⸬ $y ⸬ $l) in
+    merge $≤ (mergesort $≤ (s ₁)) (mergesort $≤ (s ₂));
+
+assert ⊢ mergesort (≤) (3 ⸬ 1 ⸬ 4 ⸬ 1 ⸬ 5 ⸬ □) ≡ 1 ⸬ 1 ⸬ 3 ⸬ 4 ⸬ 5 ⸬ □;
+
+// Two-step induction and case analysis on lists,
+// for the functions recursing by pairs
+
+opaque symbol ind_𝕃2 [a] (p : 𝕃 a → Prop) :
+  π (p □) → (Π x, π (p (x ⸬ □))) →
+  (Π x y l, π (p l) → π (p (x ⸬ y ⸬ l))) → Π l, π (p l) ≔
+begin
+  assume a p h0 h1 ih l;
+  have enough : π (p l ∧ `∀ x, p (x ⸬ l)) → π (p l) { assume h; refine ∧ₑ₁ h };
+  refine enough _;
+  remove enough;
+  generalize l;
+  induction
+  { apply ∧ᵢ h0 h1 }
+  { assume y l ihl;
+    apply ∧ᵢ
+    { refine ∧ₑ₂ ihl y }
+    { assume x; refine ih x y l (∧ₑ₁ ihl) } }
+end;
+
+opaque symbol case_𝕃2 [a] (p : 𝕃 a → Prop) :
+  π (p □) → (Π x, π (p (x ⸬ □))) →
+  (Π x y l, π (p (x ⸬ y ⸬ l))) → Π l, π (p l) ≔
+begin
+  assume a p h0 h1 h2;
+  refine ind_𝕃2 p h0 h1 _;
+  assume x y l ihl; refine h2 x y l
+end;
+
+// Strong induction on the length of a list
+
+opaque symbol ind_𝕃_size [a] (p : 𝕃 a → Prop) :
+  (Π l, (Π l', π (istrue (size l' < size l)) → π (p l')) → π (p l)) → Π l, π (p l) ≔
+begin
+  assume a p ih;
+  have aux : Π n, Π l, π (istrue (size l ≤ n)) → π (p l)
+  { refine ind_ℕ_strong (λ n, `∀ l, istrue (size l ≤ n) ⇒ p l) _;
+    assume n rec l h;
+    refine ih l _;
+    assume l' h';
+    refine rec (size l') (@leq_trans (size l' +1) (size l) n h' h) l' (≤_refl (size l')) };
+  assume l; refine aux (size l) l (≤_refl (size l))
+end;
+
+// split preserves size and multiplicities
+
+opaque symbol size_split [a] (l : 𝕃 a) :
+  π (size ((split l)₁) + size ((split l)₂) = size l) ≔
+begin
+  assume a;
+  refine ind_𝕃2 (λ l, size ((split l)₁) + size ((split l)₂) = size l) _ _ _
+  { reflexivity }
+  { assume x; reflexivity }
+  { assume x y l ih; simplify; rewrite addnS; rewrite ih; reflexivity }
+end;
+
+opaque symbol count_split [a] p (l : 𝕃 a) :
+  π (count p ((split l)₁) + count p ((split l)₂) = count p l) ≔
+begin
+  assume a p;
+  refine ind_𝕃2 (λ l, count p ((split l)₁) + count p ((split l)₂) = count p l) _ _ _
+  { reflexivity }
+  { assume x; simplify; rewrite addn0; reflexivity }
+  { assume x y l ih; simplify;
+    refine ∨ₑ (case_𝔹 (p x)) _ _
+    { assume hx; rewrite hx; simplify;
+      refine ∨ₑ (case_𝔹 (p y)) _ _
+      { assume hy; rewrite hy; simplify; rewrite addnS; rewrite ih; reflexivity }
+      { assume hy; rewrite hy; simplify; rewrite ih; reflexivity } }
+    { assume hx; rewrite hx; simplify;
+      refine ∨ₑ (case_𝔹 (p y)) _ _
+      { assume hy; rewrite hy; simplify; rewrite addnS; rewrite ih; reflexivity }
+      { assume hy; rewrite hy; simplify; rewrite ih; reflexivity } } }
+end;
+
+// Each half returned by split is no longer than the list
+
+opaque symbol size_split1 [a] (l : 𝕃 a) : π (istrue (size ((split l)₁) ≤ size l)) ≔
+begin
+  assume a l; rewrite left size_split l;
+  refine leq_addr (size ((split l)₂)) (size ((split l)₁))
+end;
+
+opaque symbol size_split2 [a] (l : 𝕃 a) : π (istrue (size ((split l)₂) ≤ size l)) ≔
+begin
+  assume a l; rewrite left size_split l;
+  refine leq_addl (size ((split l)₁)) (size ((split l)₂))
+end;
+
+// merge preserves size and multiplicities
+
+opaque symbol size_merge [a] (≤ : τ a → τ a → 𝔹) l1 l2 :
+  π (size (merge (≤) l1 l2) = size l1 + size l2) ≔
+begin
+  assume a ≤;
+  induction
+  { assume l2; reflexivity }
+  { assume x l1 ih1;
+    induction
+    { simplify; rewrite addn0; reflexivity }
+    { assume y l2 ih2;
+      refine ∨ₑ (case_𝔹 ((≤) x y)) _ _
+      { assume h; simplify; rewrite h; simplify;
+        rewrite ih1 (y ⸬ l2); reflexivity }
+      { assume h; simplify; rewrite h; simplify;
+        rewrite ih2; rewrite addnS; reflexivity } } }
+end;
+
+opaque symbol count_merge [a] p (≤ : τ a → τ a → 𝔹) l1 l2 :
+  π (count p (merge (≤) l1 l2) = count p l1 + count p l2) ≔
+begin
+  assume a p ≤;
+  induction
+  { assume l2; reflexivity }
+  { assume x l1 ih1;
+    induction
+    { simplify; rewrite addn0; reflexivity }
+    { assume y l2 ih2;
+      refine ∨ₑ (case_𝔹 ((≤) x y)) _ _
+      { assume h; simplify; rewrite h; simplify;
+        rewrite ih1 (y ⸬ l2);
+        refine ∨ₑ (case_𝔹 (p x)) _ _
+        { assume hx; rewrite hx; simplify; reflexivity }
+        { assume hx; rewrite hx; simplify; reflexivity } }
+      { assume h; simplify; rewrite h; simplify;
+        rewrite ih2;
+        refine ∨ₑ (case_𝔹 (p y)) _ _
+        { assume hy; rewrite hy; simplify; rewrite addnS; reflexivity }
+        { assume hy; rewrite hy; simplify; reflexivity } } } }
+end;
+
+// mergesort preserves size and multiplicities: its result is a permutation
+
+opaque symbol size_mergesort [a] (≤ : τ a → τ a → 𝔹) (l : 𝕃 a) :
+  π (size (mergesort (≤) l) = size l) ≔
+begin
+  assume a ≤;
+  refine ind_𝕃_size (λ l, size (mergesort (≤) l) = size l) _;
+  refine case_𝕃2
+    (λ l, (`∀ l' : τ (list a), istrue (size l' < size l)
+             ⇒ size (mergesort (≤) l') = size l')
+          ⇒ size (mergesort (≤) l) = size l) _ _ _
+  { reflexivity }
+  { reflexivity }
+  { assume x y l rec; simplify;
+    rewrite size_merge;
+    rewrite rec (x ⸬ ((split l)₁)) (size_split1 l);
+    rewrite rec (y ⸬ ((split l)₂)) (size_split2 l);
+    simplify; rewrite addnS; rewrite size_split; reflexivity }
+end;
+
+opaque symbol count_mergesort [a] p (≤ : τ a → τ a → 𝔹) (l : 𝕃 a) :
+  π (count p (mergesort (≤) l) = count p l) ≔
+begin
+  assume a p ≤;
+  refine ind_𝕃_size (λ l, count p (mergesort (≤) l) = count p l) _;
+  refine case_𝕃2
+    (λ l, (`∀ l' : τ (list a), istrue (size l' < size l)
+             ⇒ count p (mergesort (≤) l') = count p l')
+          ⇒ count p (mergesort (≤) l) = count p l) _ _ _
+  { reflexivity }
+  { reflexivity }
+  { assume x y l rec; simplify;
+    rewrite count_merge;
+    rewrite rec (x ⸬ ((split l)₁)) (size_split1 l);
+    rewrite rec (y ⸬ ((split l)₂)) (size_split2 l);
+    simplify;
+    refine ∨ₑ (case_𝔹 (p x)) _ _
+    { assume hx; rewrite hx; simplify;
+      refine ∨ₑ (case_𝔹 (p y)) _ _
+      { assume hy; rewrite hy; simplify; rewrite addnS; rewrite count_split; reflexivity }
+      { assume hy; rewrite hy; simplify; rewrite count_split; reflexivity } }
+    { assume hx; rewrite hx; simplify;
+      refine ∨ₑ (case_𝔹 (p y)) _ _
+      { assume hy; rewrite hy; simplify; rewrite addnS; rewrite count_split; reflexivity }
+      { assume hy; rewrite hy; simplify; rewrite count_split; reflexivity } } }
+end;
+
+opaque symbol all_true [a] (≤ : τ a → τ a → 𝔹) (≤_refl : Π x, π (≤ x x))
+  (p : τ a → 𝔹) (l : 𝕃 a) :
+  (Π x, π (∈ (≤) x l) → π (p x)) → π (all p l) ≔
+begin
+  assume a ≤ ≤_refl p;
+  induction
+  { assume h; refine ⊤ᵢ }
+  { assume y l ih h;
+    have hy : π (p y) { refine h y (orᵢ₁ (∈ (≤) y l) (≤_refl y)) };
+    simplify; rewrite istrue=true hy; simplify;
+    refine ih (λ x hx, h x (orᵢ₂ ((≤) x y) hx)) }
+end;
+
+opaque symbol perm_eq_mergesort [a] (≤ : τ a → τ a → 𝔹) (l : 𝕃 a) :
+  π (perm_eq (λ x y, (≤) x y and (≤) y x) (mergesort (≤) l) l) ≔
+begin
+  assume a ≤ l;
+  refine all_true (λ _ _, true) (λ _, ⊤ᵢ)
+    (λ x, eqn (count (λ y, ≤ x y and ≤ y x) (mergesort ≤ l))
+              (count (λ y, ≤ x y and ≤ y x) l))
+    ((mergesort ≤ l) ++ l) _;
+  assume x hx;
+  rewrite count_mergesort (λ y, (≤) x y and (≤) y x) (≤) l;
+  refine eqn_refl (count (λ y, (≤) x y and (≤) y x) l)
+end;
diff --git a/Nat.lp b/Nat.lp
index 4d23901..d41423b 100644
--- a/Nat.lp
+++ b/Nat.lp
@@ -94,6 +94,49 @@ inductive ℕ : TYPE ≔
 | _0 : ℕ
 | +1 : ℕ → ℕ; notation +1 postfix 100;
 
+// enable printing of natural numbers in decimal notation
+builtin "nat_zero" ≔ _0;
+builtin "nat_succ" ≔ +1;
+
+// shortcuts
+symbol _1 ≔ _0 +1;
+symbol _2 ≔ _1 +1;
+symbol _3 ≔ _2 +1;
+symbol _4 ≔ _3 +1;
+symbol _5 ≔ _4 +1;
+symbol _6 ≔ _5 +1;
+symbol _7 ≔ _6 +1;
+symbol _8 ≔ _7 +1;
+symbol _9 ≔ _8 +1;
+symbol _10 ≔ _9 +1;
+
+// Induction principle for nats from n to n+2
+opaque symbol ind_ℕ2 (p : ℕ → Prop) : π (p _0) → π (p (_0 +1)) → (Π x0: ℕ, π (p x0) → π (p (x0 +1)) → π (p (x0 +1 +1))) → Π x: ℕ, π (p x) ≔
+begin
+  assume p h0 h1 ih x;
+  have enough: π (p x ∧ p (x +1)) → π (p x) { assume h; refine ∧ₑ₁ h };
+  refine enough _;
+  remove enough;
+  generalize x;
+  induction
+  { apply ∧ᵢ h0 h1 }
+  {
+    assume x ihx;
+    apply ∧ᵢ
+    { refine ∧ₑ₂ ihx }
+    { apply ih x (∧ₑ₁ ihx) (∧ₑ₂ ihx) }
+  }
+end;
+
+// Perform just a case analysis without induction hypothesis
+opaque symbol case_ℕ (p : ℕ → Prop) : π (p _0) → (Π x: ℕ, π (p (x +1))) → Π x: ℕ, π (p x) ≔
+begin
+  assume p h1 h2;
+  induction
+  {refine h1}
+  {assume x h3;apply h2}
+end;
+
 // set code for ℕ
 
 constant symbol nat : Set;
@@ -208,6 +251,13 @@ begin
   { assume x' h y; simplify; rewrite h; reflexivity }
 end;
 
+opaque symbol suc=+1 x : π ((x +1) = (x + _1))≔
+begin
+  induction
+    {reflexivity}
+    {assume n h; rewrite h; rewrite left addSn; rewrite h; reflexivity;}
+end;
+
 opaque symbol add1n n : π ((_0 +1) + n = n +1) ≔
 begin
   assume n; reflexivity;
@@ -332,20 +382,52 @@ begin
 }
 end;
 
-opaque symbol odd≠even p q : π((p + p) +1 ≠ q + q) ≔
+symbol even: ℕ → 𝔹;
+rule even _0 ↪ true
+with even (_0 +1) ↪ false
+with even ($x +1 +1) ↪ even $x;
+
+symbol odd (n: ℕ): 𝔹 ≔ not (even n);
+
+opaque symbol evenS n : π (even (n +1) = not (even n)) ≔
 begin
   induction
-  { induction
-    { refine s≠0 }
-    { assume x h; simplify; assume i;
-      have j: π (_0 = (x + x) +1) { rewrite left addnS x x; apply +1_inj i };
-      apply 0≠s j }
-  }
-  { assume x h; induction
-    { refine s≠0 }
-    { assume y i j; apply h y; rewrite left addnS x x; apply +1_inj;
-      rewrite left addnS y y; apply +1_inj j }
-  }
+  { reflexivity }
+  { assume n ih; simplify; rewrite ih; rewrite notK; reflexivity }
+end;
+
+opaque symbol oddS n : π (odd (n +1) = not (odd n)) ≔
+begin
+  assume n; simplify; rewrite evenS; reflexivity
+end;
+
+opaque symbol even_odd n : π (even n = not (odd n)) ≔
+begin
+  assume n; simplify; symmetry; apply notK
+end;
+
+opaque symbol even_addnn n : π (even (n + n)) ≔
+begin
+  induction
+  { apply ⊤ᵢ }
+  { assume n ih; rewrite addnS; apply ih }
+end;
+
+opaque symbol odd_addnnS n : π (odd ((n + n) +1)) ≔
+begin
+  assume n; rewrite evenS; rewrite notK; refine even_addnn n
+end;
+
+opaque symbol odd≠even m n : π (odd m) → π (even n) → π (m ≠ n) ≔
+begin
+  assume m n hm hn h;
+  refine istrue_not hm (ind_eq h (λ z, istrue (even z)) hn)
+end;
+
+opaque symbol addnnS≠addnn p q : π ((p + p) +1 ≠ q + q) ≔
+begin
+  assume p q;
+  refine odd≠even ((p + p) +1) (q + q) (odd_addnnS p) (even_addnn q)
 end;
 
 // substraction
@@ -524,6 +606,11 @@ begin
   { assume x' h y; simplify; rewrite h; rewrite addnAC; reflexivity }
 end;
 
+opaque symbol muln2 n: π (n * _2 = n + n) ≔
+begin
+assume n; simplify; rewrite mulnS; rewrite muln1; reflexivity
+end;
+
 opaque symbol mulnSr x y : π (x * (y +1) = x * y + x) ≔
 begin
   induction
@@ -619,6 +706,22 @@ begin
   };
 end;
 
+// enable parsing of decimal notation
+
+builtin "0" ≔ _0;
+builtin "1" ≔ _1;
+builtin "2" ≔ _2;
+builtin "3" ≔ _3;
+builtin "4" ≔ _4;
+builtin "5" ≔ _5;
+builtin "6" ≔ _6;
+builtin "7" ≔ _7;
+builtin "8" ≔ _8;
+builtin "9" ≔ _9;
+builtin "10" ≔ _10;
+builtin "+" ≔ +;
+builtin "*" ≔ *;
+
 // Boolean ordering functions
 
 symbol ≤ : ℕ → ℕ → 𝔹; notation ≤ infix left 10;
@@ -1082,6 +1185,20 @@ begin
   apply @leq_trans (m1 - n1) (m2 - n1) (m2 - n2) t u;
 end;
 
+opaque symbol leq_exD n m : π (n ≤ m) → π (`∃ p, n + p = m) ≔
+begin
+  assume n m h;
+  refine ∨ₑ (∧ₑ₁ (leq_eqVlt n m) h) _ _
+  { assume heq; refine ∃ᵢ _0 _; simplify; rewrite addn0; refine heq }
+  { assume hnltm; refine ∃ᵢ (m - n) _; refine subnKC n m h };
+end;
+
+opaque symbol exD_leq n m : π (`∃ p, n + p = m) → π (n ≤ m) ≔
+begin
+  assume n m h; refine ∃ₑ h _; assume p h2; remove h;
+  rewrite left h2; refine leq_addr p n;
+end;
+
 // max
 
 symbol max: ℕ → ℕ → ℕ;
@@ -1781,44 +1898,354 @@ begin
   { assume n h; rewrite factS n; apply leq_pmulr (n +1) (n !) (fact_gt0 n) }
 end;
 
-// enable printing of natural numbers in decimal notation
 
-builtin "nat_zero" ≔ _0;
-builtin "nat_succ" ≔ +1;
+// Division by two i.e half
 
-// shortcuts
+symbol div2 : ℕ → ℕ;
+rule div2 _0 ↪ _0
+with div2 (_0 +1) ↪ _0
+with div2 (($x +1) +1) ↪ (div2 $x) +1;
 
-symbol _1 ≔ _0 +1;
-symbol _2 ≔ _1 +1;
-symbol _3 ≔ _2 +1;
-symbol _4 ≔ _3 +1;
-symbol _5 ≔ _4 +1;
-symbol _6 ≔ _5 +1;
-symbol _7 ≔ _6 +1;
-symbol _8 ≔ _7 +1;
-symbol _9 ≔ _8 +1;
-symbol _10 ≔ _9 +1;
+opaque symbol mul2n n : π (2 * n = n + n) ≔
+begin
+  assume n; rewrite mulnC; refine muln2 n
+end;
 
-opaque symbol suc=+1 x : π ((x +1) = (x + _1))≔
+opaque symbol div2_addnn x : π (div2 (x + x) = x) ≔
 begin
   induction
-    {reflexivity}
-    {assume n h; rewrite h; rewrite left addSn; rewrite h; reflexivity;}
+  {reflexivity}
+  { assume x ih; simplify; rewrite addnS; apply feq (+1); apply ih }
 end;
 
-// enable parsing of natural numbers in decimal notation
+opaque symbol div2_mul2n x : π ((div2 (2 * x)) = x) ≔
+begin
+  assume x; rewrite mul2n; refine div2_addnn x
+end;
 
-builtin "0" ≔ _0;
-builtin "1" ≔ _1;
-builtin "2" ≔ _2;
-builtin "3" ≔ _3;
-builtin "4" ≔ _4;
-builtin "5" ≔ _5;
-builtin "6" ≔ _6;
-builtin "7" ≔ _7;
-builtin "8" ≔ _8;
-builtin "9" ≔ _9;
-builtin "10" ≔ _10;
+opaque symbol div2_addnnS x : π (div2 ((x + x) +1) = x) ≔
+begin
+  induction
+  {reflexivity}
+  { assume x ih; simplify; rewrite addnS; apply feq (+1); apply ih }
+end;
 
-builtin "+" ≔ +;
-builtin "*" ≔ *;
+opaque symbol div2_mul2nS n : π ( div2 ((2 * n) +1) = n) ≔
+begin
+  assume n; rewrite mul2n; refine div2_addnnS n
+end;
+
+opaque symbol leq_div2 n : π (div2 (n) ≤ n) ≔
+begin
+  refine ind_ℕ2 (λ u, istrue (div2 u ≤ u)) _ _ _
+  {apply ⊤ᵢ }
+  {apply ⊤ᵢ }
+  {
+    assume x;
+    assume ih ih2;
+    apply @leq_trans (div2 x) x (x +1)
+    {refine ih}
+    {
+      refine leqnSn x
+    }
+  }
+end;
+
+opaque symbol leq_div2Sn n : π (div2 (n +1) ≤ n) ≔
+begin
+  induction
+  {apply ⊤ᵢ }
+  { assume x ih; refine leq_div2 x }
+end;
+
+opaque symbol leq_div2_leqS a n : π (a ≤ n +1) → π (div2 a ≤ n) ≔
+begin
+  induction
+  { assume n h; apply ⊤ᵢ }
+  {
+    assume a ih n h;
+    apply @leq_trans (div2 (a +1)) a n (leq_div2Sn a) h
+  }
+end;
+
+// div2 recovers the number from its parity
+
+opaque symbol even_div2 n : π (even n) → π (div2 n + div2 n = n) ≔
+begin
+  refine ind_ℕ2 (λ u, istrue (even u) ⇒ (div2 u + div2 u = u)) _ _ _
+  { assume h; reflexivity }
+  { assume h; apply ⊥ₑ h }
+  { assume x ihx ihx1 h; simplify; rewrite addnS; rewrite ihx h; reflexivity }
+end;
+
+opaque symbol odd_div2 n : π (odd n) → π ((div2 n + div2 n) +1 = n) ≔
+begin
+  refine ind_ℕ2 (λ u, istrue (odd u) ⇒ ((div2 u + div2 u) +1 = u)) _ _ _
+  { assume h; apply ⊥ₑ h }
+  { assume h; reflexivity }
+  { assume x ihx ihx1 h; simplify; rewrite addnS; rewrite ihx h; reflexivity }
+end;
+
+// Bitwise operations
+
+symbol double x ≔ x + x;
+
+// shift left
+// left-shifting a natural `x` with a natural `y` is equivalent to multiplying `x` by 2 raised to power `y`.
+symbol <<<: ℕ → ℕ → ℕ; notation <<< infix 30;
+rule $x <<< 0 ↪ $x
+with $x <<< ($n +1) ↪ double ($x <<< $n);
+
+symbol <<: ℕ → ℕ ≔ λ x, x <<< 1 ; notation << postfix 30;
+
+assert ⊢ 21 <<< 1 ≡ 42;
+
+// shift right
+// x >>> y ↪ x / (2 ^ y)
+symbol >>>: ℕ → ℕ → ℕ; notation >>> infix 30;
+rule $x >>> 0 ↪ $x
+with $x >>> ($n +1) ↪ div2 ($x >>> $n);
+
+symbol >>: ℕ → ℕ ≔ λ x, x >>> 1 ; notation >> postfix 30;
+
+assert ⊢ 21 >>> 2 ≡ 5;
+
+symbol bitwise : (𝔹 → 𝔹 → 𝔹) → ℕ → ℕ → ℕ → ℕ;
+
+rule bitwise _ _0 _ _ ↪ _0
+with bitwise $op ($n +1) $a $b ↪
+  (if ($op (odd $a) (odd $b)) 1 0) + 2 * bitwise $op $n (div2 $a) (div2 $b);
+
+symbol && (a b: ℕ): ℕ ≔ bitwise (and) a a b; notation && infix 10;
+
+symbol ⎪⎪ (a b: ℕ): ℕ ≔ bitwise (or) (max a b) a b; notation ⎪⎪ infix 12;
+
+assert ⊢ 2 ⎪⎪ 8 ≡ 10;
+
+symbol diff (a b: ℕ): ℕ ≔ bitwise (λ b1, λ b2,  b1 and (not b2)) a a b;
+
+symbol xor (a b: ℕ): ℕ ≔ bitwise (xorb) (max a b) a b; notation xor infix 10;
+
+symbol testbit (a n: ℕ) : 𝔹;
+rule testbit $a 0 ↪ odd $a
+with testbit $a ($n +1) ↪ testbit (div2 $a) $n;
+
+symbol testbit_0_l n : π (testbit 0 n = false) ≔
+begin induction { reflexivity } { assume x ih; apply ih } end;
+
+symbol Odd n ≔ (`∃ k, (2 * k + 1) = n);
+
+symbol Odd2 n : π (Odd n) → π (Odd (n + 2));
+
+symbol odd_spec n : π (Odd n) → π (odd n = true);
+
+symbol Even n ≔ (`∃ k, 2 * k = n);
+
+symbol even_spec n : π (Even n) → π (even n = true);
+
+symbol odd_bitwise op n a b : π (odd (bitwise op (n +1) a b) = op (odd a) (odd b)) ≔
+begin
+  assume op n a b;
+  simplify bitwise;
+  have case: π (
+    (op (odd a) (odd b) = true)
+    ∨
+    (op (odd a) (odd b) = false)) { apply case_𝔹 };
+  apply ∨ₑ case
+  {
+    assume hl; rewrite hl; simplify if;
+    rewrite addnC;
+    apply odd_spec ((_2 * bitwise op n (div2 a) (div2 b)) + _1);
+    apply ∃ᵢ (bitwise op n (div2 a) (div2 b));
+    reflexivity
+  }
+  {
+    assume hr; rewrite hr; simplify if;
+    simplify; rewrite addn0;
+    refine @feq bool bool not (even (bitwise op n (div2 a) (div2 b) + bitwise op n (div2 a) (div2 b))) true _;
+    apply even_spec (bitwise op n (div2 a) (div2 b) + bitwise op n (div2 a) (div2 b));
+    refine ∃ᵢ (bitwise op n (div2 a) (div2 b)) (mul2n (bitwise op n (div2 a) (div2 b)))
+  }
+end;
+
+symbol div2_bitwise op n a b :
+  π (div2 (bitwise op (n +1) a b) = bitwise op n (div2 a) (div2 b)) ≔
+begin
+  assume op n a b;
+  simplify bitwise;
+  have case: π (
+    (op (odd a) (odd b) = true)
+    ∨
+    (op (odd a) (odd b) = false)) { apply case_𝔹 };
+  apply ∨ₑ case
+  {
+    assume hl; rewrite hl; simplify if;
+    rewrite addnC; simplify; rewrite addn1;
+    apply div2_mul2nS
+  }
+  {
+    assume hr; rewrite hr; simplify if;
+    apply div2_mul2n (bitwise op n (div2 a) (div2 b))
+  }
+end;
+
+symbol testbit_bitwise_1 op (hop : Π b, π (op false b = false)) n m a b :
+  π (a ≤ n) →
+  π (testbit (bitwise op n a b) m = op (testbit a m) (testbit b m))
+≔ begin
+  assume op Hop;
+  induction
+  {
+     assume m a b Ha;
+    rewrite ≤0 a Ha;
+    simplify;
+    rewrite testbit_0_l;
+    rewrite Hop ((testbit b m));
+    reflexivity
+  }
+  {
+    assume n IHn;
+    induction
+    {
+      assume a b ha;
+      apply odd_bitwise op (n) a b
+    }
+    {
+      assume m Ihm a b ha;
+      simplify testbit;
+      rewrite div2_bitwise;
+      apply IHn m (div2 a) (div2 b) _;
+      refine  leq_div2_leqS a n ha
+    }
+  }
+end;
+
+symbol testbit_bitwise_2 op (hop : π (op false false = false)) n m a b :
+  π (a ≤ n) → π (b ≤ n) →
+  π (testbit (bitwise op n a b) m = op (testbit a m) (testbit b m))
+≔ begin
+  assume op Hop_spec;
+  induction
+  {
+     assume m a b Ha Hb;
+    rewrite ≤0 a Ha;
+    rewrite ≤0 b Hb;
+    simplify;
+    rewrite testbit_0_l;
+    symmetry;
+    apply Hop_spec
+  }
+  {
+    assume n IHn;
+    induction
+    {
+      assume a b ha hb;
+      apply odd_bitwise op (n) a b;
+    }
+    {
+      assume m Ihm a b ha hb;
+      simplify testbit;
+      rewrite div2_bitwise;
+      apply IHn m (div2 a) (div2 b) _ _
+      { refine  leq_div2_leqS a n ha }
+      { refine  leq_div2_leqS b n hb }
+    }
+  }
+end;
+
+symbol land_spec a b n :
+  π (testbit (a && b) n = (testbit a n and testbit b n)) ≔
+begin
+  assume a n b;
+  simplify;
+  refine testbit_bitwise_1 (and) _ a b a n (≤_refl a);
+  induction
+  {reflexivity}
+  {reflexivity}
+end;
+
+symbol ldiff_spec a b n :
+  π (testbit (diff a b) n = (testbit a n and not (testbit b n))) ≔
+begin
+  assume a n b;
+  simplify diff;
+  refine testbit_bitwise_1 (λ a b, a and not b) _ a b a n (≤_refl a);
+  induction
+  {reflexivity}
+  {reflexivity}
+end;
+
+symbol lor_spec a b n :
+  π (testbit (a ⎪⎪ b) n = (testbit a n or testbit b n)) ≔
+begin
+  assume a n b;
+  simplify;
+  refine  testbit_bitwise_2 (or) _ (max a n) b a n _ _
+  {reflexivity}
+  {refine leq_maxl a n }
+  {refine leq_maxr a n }
+end;
+
+symbol xor_spec a b n :
+  π (testbit (a xor b) n = (testbit a n xorb testbit b n)) ≔
+begin
+ assume a n b;
+  simplify;
+  refine  testbit_bitwise_2 (xorb) _ (max a n) b a n _ _
+  {reflexivity}
+  {refine leq_maxl a n }
+  {refine leq_maxr a n }
+end;
+
+opaque symbol shiftr_spec a n m : π (testbit (a >>> n) m = testbit a (m + n)) ≔
+begin
+  assume a;
+  induction
+  { assume m; rewrite addn0; reflexivity }
+  {
+    assume n ihn m;
+    rewrite addnS;
+    refine ihn (m +1)
+  }
+end;
+
+opaque symbol shiftl_spec a n m : π (n ≤ m) → π (testbit (a <<< n) m = testbit a (m - n)) ≔
+begin
+assume a;
+  induction
+  { assume m h; rewrite sub0n; reflexivity }
+  {
+    assume n ih;
+    induction
+    {
+      assume contra;
+      apply ⊥ₑ contra
+    }
+    {
+      assume m ihm h;
+      remove ihm;
+      simplify;
+      rewrite left (ih m h);
+      have g: π ((((a <<< n) + (a <<< n))) = (2 * (a <<< n)))
+        { symmetry; refine mul2n (a <<< n) };
+      rewrite g;
+      rewrite div2_mul2n;
+      reflexivity
+    }
+  }
+end;
+
+// Strong (course-of-values) induction
+
+opaque symbol ind_ℕ_strong (p : ℕ → Prop) :
+  (Π n, (Π m, π (istrue (m < n)) → π (p m)) → π (p n)) → Π n, π (p n) ≔
+begin
+  assume p ih n;
+  have aux : Π k, Π m, π (istrue (m ≤ k)) → π (p m)
+  { induction
+    { assume m h; rewrite ≤0 m h; refine ih _0 _;
+      assume m' h'; apply ⊥ₑ; refine ltn0 m' h' }
+    { assume k rec m h; refine ih m _;
+      assume m' h'; refine rec m' (@leq_trans (m' +1) m (k +1) h' h) } };
+  refine aux n n (≤_refl n)
+end;
diff --git a/Pos.lp b/Pos.lp
index 2a60405..a7b4427 100644
--- a/Pos.lp
+++ b/Pos.lp
@@ -153,7 +153,7 @@ begin
     { simplify; assume y i j; apply ⊥ₑ;
       have H: π ((((val x + (val x + 0)) +1) = (val y + (val y + 0))) ⇒ (((val x + val x) +1) = (val y + val y)))
         {rewrite addn0; rewrite addn0; assume h0; refine h0};
-      apply odd≠even (val x) (val y) (H j) }
+      apply addnnS≠addnn (val x) (val y) (H j) }
     { simplify; assume i; apply ⊥ₑ; apply 2*val≠0 x; apply +1_inj;
       have H: π ((((val x + (val x + 0)) +1) = 1) ⇒ (((val x + val x) +1) = 1))
         {rewrite addn0; assume h0; refine h0};
@@ -163,12 +163,12 @@ begin
     { simplify; assume y i j; apply ⊥ₑ;
     have H: π (((val x + (val x + 0)) = ((val y + (val y + 0)) +1)) ⇒ ((val x + val x) = ((val y + val y) +1)))
         {rewrite addn0; rewrite addn0; assume h0; refine h0};
-      apply odd≠even (val y) (val x) (eq_sym (H j)) }
+      apply addnnS≠addnn (val y) (val x) (eq_sym (H j)) }
     { simplify; assume y i j; apply feq O; apply h; apply 2*_inj;
       have H: π (((val x + (val x + 0)) = (val y + (val y + 0))) ⇒ ((val x + val x) = (val y + val y)))
         {rewrite addn0; rewrite addn0; assume h0; refine h0};
     apply (H j) }
-    { assume i; apply ⊥ₑ; apply odd≠even 0 (val x); symmetry; simplify;
+    { assume i; apply ⊥ₑ; apply addnnS≠addnn 0 (val x); symmetry; simplify;
       have H: π ((val (O x) = val H) ⇒ ((val x + val x) = 1))
         {simplify val; simplify *; simplify *; simplify *; rewrite addn0; assume h0; refine h0};
     apply (H i)
@@ -180,7 +180,7 @@ begin
       have H: π ((1 = ((val x + (val x + 0)) +1)) ⇒ (1 = ((val x + val x) +1)))
         {rewrite addn0; assume h0; refine h0};
       apply (H i) }
-    { simplify; assume x h i; apply ⊥ₑ; apply odd≠even 0 (val x); simplify;
+    { simplify; assume x h i; apply ⊥ₑ; apply addnnS≠addnn 0 (val x); simplify;
       have H: π ((1 = (val x + (val x + 0))) ⇒ (1 = (val x + val x)))
         {rewrite addn0; assume h0; refine h0};
     apply (H i) }
@@ -628,6 +628,131 @@ rule mul (I $x) $y ↪ add $y (O (mul $x $y))
 with mul (O $x) $y ↪ O (mul $x $y)
 with mul H      $y ↪ $y;
 
+// Right reduction properties for multiplication
+
+opaque symbol mul_O_right p q : π (mul p (O q) = O (mul p q)) ≔
+begin
+  induction
+   { assume p prec q; simplify; rewrite prec; refine feq O _; reflexivity }
+   { assume p prec q; simplify; rewrite prec; refine feq O _; reflexivity }
+   { reflexivity }
+end;
+
+opaque symbol mul_I_right p q : π (mul p (I q) = add p (O (mul p q))) ≔
+begin
+  induction
+   { assume p prec q; simplify; refine feq I _;
+     rewrite prec; rewrite left add_assoc; rewrite add_com q p;
+     rewrite left add_assoc; reflexivity }
+   { assume p prec q; simplify; refine feq O _; rewrite prec; reflexivity }
+   { reflexivity }
+end;
+
+opaque symbol mul_H_right p : π (mul p H = p) ≔
+begin
+  induction
+   { assume p prec; simplify; rewrite prec; reflexivity }
+   { assume p prec; simplify; rewrite prec; reflexivity }
+   { reflexivity }
+end;
+
+// Commutativity of multiplication
+
+opaque symbol mul_com x y : π (mul x y = mul y x) ≔
+begin
+  induction
+   { assume x xrec y; rewrite mul_I_right; simplify; rewrite xrec y; reflexivity }
+   { assume x xrec y; rewrite mul_O_right; simplify; rewrite xrec y; reflexivity }
+   { assume y; rewrite mul_H_right; reflexivity }
+end;
+
+// Interaction of multiplication with succ
+
+opaque symbol addnn n : π (add n n = O n) ≔
+begin
+  induction
+   { assume n nrec; simplify; rewrite left succ_add n n; rewrite nrec; reflexivity }
+   { assume n nrec; simplify; rewrite nrec; reflexivity }
+   { reflexivity }
+end;
+
+opaque symbol mul_succ n m : π (mul (succ n) m = add (mul n m) m) ≔
+begin
+  induction
+   { assume n nrec m; symmetry; simplify;
+     rewrite nrec;
+     rewrite left addnn;
+     rewrite left addnn;
+     rewrite add_com (mul n m) m;
+     rewrite .[in x in _ = x] add_assoc;
+     rewrite .[in x in _ = x] add_com;
+     rewrite left add_assoc m (mul n m) (mul n m);
+     rewrite .[in x in x = _] add_com m (mul n m);
+     rewrite add_assoc (mul n m) m (mul n m);
+     reflexivity }
+   { assume n nrec m; symmetry; simplify; rewrite add_com; reflexivity }
+   { assume m; symmetry; simplify; apply addnn }
+end;
+
+opaque symbol mul_succ_right n m : π (mul n (succ m) = add (mul n m) n) ≔
+begin
+  assume n m;
+  symmetry;
+  rewrite mul_com n (succ m);
+  rewrite mul_succ m n;
+  rewrite mul_com n m;
+  reflexivity
+end;
+
+// Distributivity of multiplication over addition
+
+opaque symbol mul_distr_l a x y : π (mul a (add x y) = add (mul a x) (mul a y)) ≔
+begin
+  refine ind_ℙeano (λ a, `∀ x, `∀ y, mul a (add x y) = add (mul a x) (mul a y)) _ _
+  // case H
+  { reflexivity }
+  // case succ
+  { assume a arec x y;
+    rewrite mul_succ;
+    rewrite (arec x y);
+    rewrite mul_succ;
+    rewrite mul_succ;
+    rewrite add_assoc;
+    rewrite add_com;
+    rewrite add_com x y;
+    rewrite left add_assoc;
+    rewrite add_assoc;
+    rewrite add_com;
+    rewrite add_com x (mul a x);
+    reflexivity }
+end;
+
+opaque symbol mul_distr_r a x y : π (mul (add x y) a = add (mul x a) (mul y a)) ≔
+begin
+  assume a x y;
+  rewrite mul_com;
+  rewrite mul_com x a;
+  rewrite mul_com y a;
+  refine mul_distr_l a x y
+end;
+
+// Associativity of multiplication
+
+opaque symbol mul_assoc x y z : π (mul (mul x y) z = mul x (mul y z)) ≔
+begin
+  assume x y;
+  refine ind_ℙeano (λ z, mul (mul x y) z = mul x (mul y z)) _ _
+  // case H
+  { simplify; rewrite mul_H_right; rewrite mul_H_right; reflexivity }
+  // case succ
+  { assume z zrec;
+    rewrite mul_succ_right (mul x y) z;
+    rewrite mul_succ_right y z;
+    rewrite mul_distr_l;
+    rewrite zrec;
+    reflexivity }
+end;
+
 // enable printing of positive numbers in decimal notation
 
 builtin "pos_one" ≔ H;
diff --git a/Prod.lp b/Prod.lp
index b97126b..af2a3c3 100644
--- a/Prod.lp
+++ b/Prod.lp
@@ -1,12 +1,14 @@
 // Cartesian product
 
-require open Stdlib.Set;
+require open Stdlib.Eq;
 
-constant symbol × : Set → Set → Set; notation × infix right 10; // \times
+(a b:Set) inductive Prod:TYPE ≔ ‚ : τ a → τ b → Prod a b;
+
+notation ‚ infix right 30;
 
-assert a b c ⊢ a × b × c ≡ a × (b × c);
+constant symbol × : Set → Set → Set; notation × infix right 10; // \times
 
-symbol ‚ [a b] : τ a → τ b → τ (a × b); notation ‚ infix right 30;
+rule τ ($a × $b) ↪ Prod $a $b;
 
 assert a (x:τ a) b (y:τ b) c (z:τ c) ⊢ x ‚ y ‚ z : τ(a × b × c);
 assert x y z ⊢ x ‚ y ‚ z ≡ x ‚ (y ‚ z);
@@ -18,3 +20,69 @@ rule ($x ‚ _)₁ ↪ $x;
 symbol ₂ [a b] : τ(a × b) → τ b; notation ₂ postfix 10;
 
 rule (_ ‚ $x)₂ ↪ $x;
+
+opaque symbol eq_₁ [a b] (x y: τ (a × b)) : π (x = y) → π ((x ₁) = (y ₁)) ≔
+begin assume a b x y h; refine feq (λ z, z ₁) h end;
+
+opaque symbol eq_₂ [a b] (x y: τ (a × b)) : π (x = y) → π ((x ₂) = (y ₂)) ≔
+begin assume a b x y h; refine feq (λ z, z ₂) h end;
+
+opaque symbol ‚_inj₁ [a b] (x x': τ a) (y y': τ b) :
+  π (x ‚ y = x' ‚ y') → π (x = x') ≔
+begin assume a b x x' y y' h; refine eq_₁ (x ‚ y) (x' ‚ y') h end;
+
+opaque symbol ‚_inj₂ [a b] (x x': τ a) (y y': τ b) :
+  π (x ‚ y = x' ‚ y') → π (y = y') ≔
+begin assume a b x x' y y' h; refine eq_₂ (x ‚ y) (x' ‚ y') h end;
+
+symbol map_× [a b c d] (f: τ a → τ c) (g: τ b → τ d) (x: τ (a × b)) : τ (c × d) ≔
+  f (x ₁) ‚ g (x ₂);
+
+opaque symbol map_×_comp [a b c d e f]
+  (g: τ c → τ e) (g': τ d → τ f) (h: τ a → τ c) (h': τ b → τ d) (x: τ (a × b)) :
+  π (map_× g g' (map_× h h' x) = map_× (λ u, g (h u)) (λ v, g' (h' v)) x) ≔
+begin reflexivity end;
+
+symbol swap_× [a b] (x: τ (a × b)) : τ (b × a) ≔ (x ₂) ‚ (x ₁);
+
+symbol pairing [a b c] (f: τ c → τ a) (g: τ c → τ b) : τ c → τ (a × b) ≔
+  λ z, f z ‚ g z;
+
+opaque symbol ₁_pairing [a b c] (f: τ c → τ a) (g: τ c → τ b) (z: τ c) :
+  π ((pairing f g z ₁) = f z) ≔
+begin reflexivity end;
+
+opaque symbol ₂_pairing [a b c] (f: τ c → τ a) (g: τ c → τ b) (z: τ c) :
+  π ((pairing f g z ₂) = g z) ≔
+begin reflexivity end;
+
+symbol prodExt [a b] (x: τ (a × b)) : π (x = (x ₁) ‚ (x ₂)) ≔
+begin
+  assume a; refine ind_Prod a (λ b x, x = (x ₁) ‚ (x ₂)) _; reflexivity
+end;
+
+opaque symbol eq_pair [a b] (x y: τ (a × b)) :
+  π ((x ₁) = (y ₁)) → π ((x ₂) = (y ₂)) → π (x = y) ≔
+begin
+  assume a b x y h1 h2;
+  rewrite (prodExt x); rewrite (prodExt y);
+  refine feq2 (λ u v, u ‚ v) h1 h2
+end;
+
+opaque symbol eq_×_iff [a b] (x y: τ (a × b)) :
+  π (x = y ⇔ (x ₁) = (y ₁) ∧ (x ₂) = (y ₂)) ≔
+begin
+  assume a b x y; apply ∧ᵢ
+    { assume h; apply ∧ᵢ { refine eq_₁ x y h } { refine eq_₂ x y h } }
+    { assume h; refine eq_pair x y (∧ₑ₁ h) (∧ₑ₂ h) }
+end;
+
+opaque symbol map_×_id [a b] (x: τ (a × b)) : π (map_× (λ u, u) (λ v, v) x = x) ≔
+begin assume a b x; symmetry; refine prodExt x end;
+
+opaque symbol swap_×_invol [a b] (x: τ (a × b)) : π (swap_× (swap_× x) = x) ≔
+begin assume a b x; symmetry; refine prodExt x end;
+
+opaque symbol pairing_uniq [a b c] (h: τ c → τ (a × b)) (z: τ c) :
+  π (pairing (λ u, h u ₁) (λ u, h u ₂) z = h z) ≔
+begin assume a b c h z; symmetry; refine prodExt (h z) end;
diff --git a/Subset.lp b/Subset.lp
new file mode 100644
index 0000000..300fab9
--- /dev/null
+++ b/Subset.lp
@@ -0,0 +1,37 @@
+// Subset types: a dependent pair of an element and a proof
+
+require open Stdlib.FOL Stdlib.Eq;
+
+[a: Set] (p: τ a → Prop) inductive Subset : TYPE ≔
+  mk (x: τ a) : π (p x) → Subset p;
+
+symbol elt [a] [p:τ a → Prop] (e: Subset p) : τ a;
+
+rule elt (mk $x _) ↪ $x;
+
+symbol prf [a] [p:τ a → Prop] (e: Subset p) : π (p (elt e));
+
+rule prf (mk _ $h) ↪ $h;
+
+opaque symbol Subset_∃ [a] [p:τ a → Prop] (e: Subset p) : π (`∃ x, p x) ≔
+begin assume a p e; refine ∃ᵢ (elt e) (prf e) end;
+
+/* The `subset` Set-constructor requires an existential proof: this is needed
+   to be consistent with the axiom `el` of Set.lp stating that every set is
+   non-empty. */
+
+constant symbol subset [a] (p: τ a → Prop) : π (`∃ x, p x) → Set;
+
+rule τ (subset $p _) ↪ Subset $p;
+
+opaque symbol η_subset [a] [p:τ a → Prop] [h] (e: τ (subset p h)) :
+  π (mk (elt e) (prf e) = e) ≔
+begin assume a p h; induction; reflexivity end;
+
+opaque symbol eq_elt [a] [p:τ a → Prop] [h] (x y: τ (subset p h)) :
+  π (x = y) → π (elt x = elt y) ≔
+begin assume a p h x y e; refine feq elt e end;
+
+opaque symbol mk_inj [a] [p:τ a → Prop] [h] x y (hx: π (p x)) (hy: π (p y)) :
+  π (= [subset p h] (mk x hx) (mk y hy)) → π (x = y) ≔
+begin assume a p h x y hx hy e; refine @eq_elt a p h (mk x hx) (mk y hy) e end;
diff --git a/Z.lp b/Z.lp
index 7d9c28f..84187e1 100644
--- a/Z.lp
+++ b/Z.lp
@@ -15,6 +15,25 @@ constant symbol int : Set;
 
 rule τ int ↪ ℤ;
 
+// shortcuts
+
+symbol _1 ≔ Zpos _1;
+symbol _2 ≔ Zpos _2;
+symbol _3 ≔ Zpos _3;
+symbol _4 ≔ Zpos _4;
+symbol _5 ≔ Zpos _5;
+symbol _6 ≔ Zpos _6;
+symbol _7 ≔ Zpos _7;
+symbol _8 ≔ Zpos _8;
+symbol _9 ≔ Zpos _9;
+symbol _10 ≔ Zpos _10;
+
+// enable printing of integers in decimal notation
+
+builtin "int_zero" ≔ Z0;
+builtin "int_positive" ≔ Zpos;
+builtin "int_negative" ≔ Zneg;
+
 // boolean functions for testing head constructor
 
 symbol isZ0 : ℤ → 𝔹;
@@ -52,6 +71,14 @@ begin
   assume x y h; refine ind_eq h (λ n, istrue(isZneg n)) ⊤ᵢ
 end;
 
+// Sign
+
+symbol sign : ℤ → ℤ;
+
+rule sign Z0       ↪ Zpos H
+with sign (Zpos _) ↪ Zpos H
+with sign (Zneg _) ↪ Zneg H;
+
 // Unary opposite
 
 symbol — : ℤ → ℤ;
@@ -351,6 +378,247 @@ begin
           { assume z; simplify; rewrite add_assoc; reflexivity } } }
 end;
 
+// Compatibility of equality with the addition
+
+opaque symbol =_compat_add x y c : π (x = y) → π (x + c = y + c) ≔
+begin
+  assume x y c h; rewrite h; reflexivity
+end;
+
+opaque symbol =_sub a b : π (a - b = Z0 ⇒ a = b) ≔
+begin
+  assume a b h;
+  have g : π ((a - b) + b = b)
+  { simplify; refine =_compat_add (a - b) Z0 b h };
+  have g2 : π (a + (b - b) = b)
+  { simplify; rewrite +_com b (— b); rewrite left +_assoc; refine g };
+  rewrite left +Z0 a;
+  rewrite left -_same b;
+  refine g2
+end;
+
+// Multiplication
+
+symbol * : ℤ → ℤ → ℤ; notation * infix right 22;
+
+rule Z0      * _       ↪ Z0
+with _       * Z0       ↪ Z0
+with Zpos $x * Zpos $y ↪ Zpos (mul $x $y)
+with Zpos $x * Zneg $y ↪ Zneg (mul $x $y)
+with Zneg $x * Zpos $y ↪ Zneg (mul $x $y)
+with Zneg $x * Zneg $y ↪ Zpos (mul $x $y);
+
+opaque symbol *_com x y : π (x * y = y * x) ≔
+begin
+  induction
+  // case Z0
+  { induction { reflexivity } { reflexivity } { reflexivity } }
+  // case Zpos
+  { assume x;
+    induction
+     { reflexivity }
+     { assume y; simplify; rewrite mul_com; reflexivity }
+     { assume y; simplify; rewrite mul_com; reflexivity } }
+  // case Zneg
+  { assume x;
+    induction
+     { reflexivity }
+     { assume y; simplify; rewrite mul_com; reflexivity }
+     { assume y; simplify; rewrite mul_com; reflexivity } }
+end;
+
+opaque symbol *_assoc x y z : π ((x * y) * z = x * (y * z)) ≔
+begin
+  induction
+  // case Z0
+  { reflexivity }
+  // case Zpos
+  { assume x;
+    induction
+     { reflexivity }
+     { assume y;
+       induction
+         { reflexivity }
+         { assume z; simplify; rewrite mul_assoc; reflexivity }
+         { assume z; simplify; rewrite mul_assoc; reflexivity } }
+     { assume y;
+       induction
+         { reflexivity }
+         { assume z; simplify; rewrite mul_assoc; reflexivity }
+         { assume z; simplify; rewrite mul_assoc; reflexivity } } }
+  // case Zneg
+  { assume x;
+    induction
+     { reflexivity }
+     { assume y;
+       induction
+         { reflexivity }
+         { assume z; simplify; rewrite mul_assoc; reflexivity }
+         { assume z; simplify; rewrite mul_assoc; reflexivity } }
+     { assume y;
+       induction
+         { reflexivity }
+         { assume z; simplify; rewrite mul_assoc; reflexivity }
+         { assume z; simplify; rewrite mul_assoc; reflexivity } } }
+end;
+
+opaque symbol *_neutral x : π (x * Zpos H = x) ≔
+begin
+  induction
+  { reflexivity }
+  { assume p; simplify; rewrite mul_H_right; reflexivity }
+  { assume p; simplify; rewrite mul_H_right; reflexivity }
+end;
+
+opaque symbol *Z0 x : π (x * Z0 = Z0) ≔
+begin
+  induction { reflexivity } { reflexivity } { reflexivity }
+end;
+
+symbol neg_mul_l a b : π (— (a * b) = (— a) * b) ≔
+begin
+  induction
+  {reflexivity}
+  { assume a; induction { reflexivity } { reflexivity } { reflexivity } }
+  { assume a; induction { reflexivity } { reflexivity } { reflexivity } }
+end;
+
+symbol neg_mul_r a b : π (— (a * b) = a * — b) ≔
+begin
+  induction
+  {reflexivity}
+  { assume a; induction { reflexivity } { reflexivity } { reflexivity } }
+  { assume a; induction { reflexivity } { reflexivity } { reflexivity } }
+end;
+
+opaque symbol *_Zpos_succ (a : ℙ) (s : ℤ) : π (Zpos (succ a) * s = Zpos a * s + s) ≔
+begin
+  assume a;
+  induction
+  { reflexivity }
+  { assume b; simplify; rewrite mul_succ a b; reflexivity }
+  { assume b; simplify; rewrite mul_succ a b; reflexivity }
+end;
+
+opaque symbol sub_add_sub (p q r s : ℙ) :
+  π (sub p q + sub r s = sub (add p r) (add q s)) ≔
+begin
+  assume p q r s;
+  have e : π (sub p q + (Zpos r + Zneg s) = sub (add p r) (add q s))
+  { rewrite left +_assoc (sub p q) (Zpos r) (Zneg s);
+    rewrite sub_add_Zpos p q r; rewrite sub_add_Zneg (add p r) q s;
+    reflexivity };
+  refine e
+end;
+
+opaque symbol mul_distr_sub_pos_l (a x y : ℙ) :
+  π (Zpos a * sub x y = sub (mul a x) (mul a y)) ≔
+begin
+  assume a x y;
+  refine ind_ℙeano (λ a, Zpos a * sub x y = sub (mul a x) (mul a y)) _ _ a
+  { simplify; rewrite *_com (Zpos H) (sub x y); refine *_neutral (sub x y) }
+  { assume b IH;
+    rewrite *_Zpos_succ b (sub x y); rewrite IH;
+    rewrite sub_add_sub (mul b x) (mul b y) x y;
+    rewrite left mul_succ b x; rewrite left mul_succ b y; reflexivity }
+end;
+
+opaque symbol mul_distr_sub_neg_l (a x y : ℙ) :
+  π (Zneg a * sub x y = sub (mul a y) (mul a x)) ≔
+begin
+  assume a x y;
+  have e : π ((— Zpos a) * sub x y = sub (mul a y) (mul a x))
+  { rewrite left neg_mul_l (Zpos a) (sub x y);
+    rewrite mul_distr_sub_pos_l a x y; refine sub_opp (mul a x) (mul a y) };
+  refine e
+end;
+
+opaque symbol *_distr_l (z x y : ℤ) : π (z * (x + y) = z * x + z * y) ≔
+begin
+  induction
+  { assume x y; reflexivity }
+  { assume z;
+    induction
+    { reflexivity }
+    { assume x;
+      induction
+      { reflexivity }
+      { assume y; simplify; rewrite mul_distr_l; reflexivity }
+      { assume y; simplify; rewrite mul_distr_sub_pos_l; reflexivity } }
+    { assume x;
+      induction
+      { reflexivity }
+      { assume y; simplify; rewrite mul_distr_sub_pos_l; reflexivity }
+      { assume y; simplify; rewrite mul_distr_l; reflexivity } } }
+  { assume z;
+    induction
+    { assume x; reflexivity }
+    { assume x;
+      induction
+      { reflexivity }
+      { assume y; simplify; rewrite mul_distr_l; reflexivity }
+      { assume y; simplify; rewrite mul_distr_sub_neg_l; reflexivity } }
+    { assume x;
+      induction
+      { reflexivity }
+      { assume y; simplify; rewrite mul_distr_sub_neg_l; reflexivity }
+      { assume y; simplify; rewrite mul_distr_l; reflexivity } } }
+end;
+
+opaque symbol *_distr_r (x y z : ℤ) : π ((x + y) * z = x * z + y * z) ≔
+begin
+  assume x y z;
+  rewrite *_com (x + y) z; rewrite *_com x z; rewrite *_com y z;
+  refine *_distr_l z x y
+end;
+
+opaque symbol distr_—_*_l a b : π (— (a * b) = (— a) * b) ≔
+begin
+  induction
+  { reflexivity }
+  { assume a; induction { reflexivity } { reflexivity } { reflexivity } }
+  { assume a; induction { reflexivity } { reflexivity } { reflexivity } }
+end;
+
+opaque symbol distr_—_*_r a b : π (— (a * b) = a * — b) ≔
+begin
+  induction
+  { reflexivity }
+  { assume a; induction { reflexivity } { reflexivity } { reflexivity } }
+  { assume a; induction { reflexivity } { reflexivity } { reflexivity } }
+end;
+
+// enable parsing of integers in decimal notation
+
+builtin "0" ≔ Z0;
+builtin "1" ≔ _1;
+builtin "2" ≔ _2;
+builtin "3" ≔ _3;
+builtin "4" ≔ _4;
+builtin "5" ≔ _5;
+builtin "6" ≔ _6;
+builtin "7" ≔ _7;
+builtin "8" ≔ _8;
+builtin "9" ≔ _9;
+builtin "10" ≔ _10;
+builtin "+" ≔ +;
+builtin "*" ≔ *;
+builtin "-" ≔ —;
+
+// Exponentiation
+
+symbol power_pos (x : ℤ) (p : ℙ) : ℤ;
+
+rule power_pos $x H       ↪ $x
+with power_pos $x (O $p)  ↪ let r ≔ power_pos $x $p in r * r
+with power_pos $x (I $p)  ↪ let r ≔ power_pos $x $p in $x * r * r;
+
+symbol ^ : ℤ → ℤ → ℤ; notation ^ infix 3;
+
+rule _  ^ Z0        ↪ Zpos H
+with $x ^ (Zpos $p) ↪ power_pos $x $p
+with _  ^ (Zneg _)  ↪ Z0;
+
 // Comparison of integers
 
 require open Stdlib.Comp;
@@ -512,6 +780,49 @@ begin
      { assume y; simplify; rewrite ≐_pos_sub; rewrite compare_com; reflexivity } }
 end;
 
+opaque symbol ≐_mul_Zpos w r : π ((w * Zpos r ≐ Z0) = (w ≐ Z0)) ≔
+begin
+  induction
+   { assume r; reflexivity }
+   { assume a r; reflexivity }
+   { assume a r; reflexivity }
+end;
+
+// ℤ has no zero divisor
+
+opaque symbol *=Z0 x y : π (x * y = Z0) → π (x = Z0 ∨ y = Z0) ≔
+begin
+  induction
+  // case Z0
+  { assume y h; apply ∨ᵢ₁; reflexivity }
+  // case Zpos
+  { assume a;
+    induction
+     { assume h; apply ∨ᵢ₂; reflexivity }
+     { assume b h; apply ⊥ₑ (Zpos≠Z0 (mul a b) h) }
+     { assume b h; apply ⊥ₑ (Zneg≠Z0 (mul a b) h) } }
+  // case Zneg
+  { assume a;
+    induction
+     { assume h; apply ∨ᵢ₂; reflexivity }
+     { assume b h; apply ⊥ₑ (Zneg≠Z0 (mul a b) h) }
+     { assume b h; apply ⊥ₑ (Zpos≠Z0 (mul a b) h) } }
+end;
+
+opaque symbol ≐_refl x : π (x ≐ x = Eq) ≔
+begin
+  induction
+  { reflexivity }
+  { induction
+     { assume x H; refine H }
+     { assume x H; refine H }
+     { reflexivity } }
+  { induction
+     { assume x H; refine H }
+     { assume x H; refine H }
+     { reflexivity } }
+end;
+
 // Compatibility of comparison with the addition
 
 opaque symbol ≐_compat_add x y z : π ((x ≐ y) = (x + z ≐ y + z)) ≔
@@ -523,6 +834,45 @@ begin
   rewrite -_same z; reflexivity;
 end;
 
+opaque symbol ≐_compat_mul x y r : π ((x ≐ y) = (x * Zpos r ≐ y * Zpos r)) ≔
+begin
+  assume x y r;
+  rewrite ≐_sub x y;
+  rewrite ≐_sub (x * Zpos r) (y * Zpos r);
+  rewrite distr_—_*_l y (Zpos r);
+  rewrite left *_distr_r x (— y) (Zpos r);
+  rewrite ≐_mul_Zpos (x + — y) r;
+  reflexivity
+end;
+
+// Regularity of multiplication
+
+opaque symbol *_reg_r x y k : π (k ≠ Z0 ⇒ x * k = y * k ⇒ x = y) ≔
+begin
+  assume x y;
+  induction
+  // case Z0
+  { assume h0 h; apply ⊥ₑ; refine h0 (eq_refl Z0) }
+  // case Zpos
+  { assume r h0 h;
+    refine ≐_decides x y _;
+    rewrite ≐_compat_mul x y r;
+    rewrite h;
+    refine ≐_refl (y * Zpos r) }
+  // case Zneg
+  { assume r h0 h;
+    have ex : π (x * Zpos r = — (x * Zneg r))
+    { symmetry; refine distr_—_*_r x (Zneg r) };
+    have ey : π (y * Zpos r = — (y * Zneg r))
+    { symmetry; refine distr_—_*_r y (Zneg r) };
+    have h2 : π (x * Zpos r = y * Zpos r)
+    { rewrite ex; rewrite ey; rewrite h; reflexivity };
+    refine ≐_decides x y _;
+    rewrite ≐_compat_mul x y r;
+    rewrite h2;
+    refine ≐_refl (y * Zpos r) }
+end;
+
 // Directional comparison operators
 
 symbol ≤ x y ≔ ¬ (istrue(isGt(x ≐ y)));
@@ -546,6 +896,31 @@ begin
    { refine (λ x _, x) }
 end;
 
+opaque symbol <_¬_≤ x y : π (x < y ⇒ ¬ (y ≤ x)) ≔
+begin
+  assume x y;
+  simplify;
+  have e : π (istrue (isLt (x ≐ y)) ⇒ ¬ ¬ (istrue (isGt (y ≐ x))))
+  { rewrite ≐_com y x };
+  refine ind_Comp (λ c, istrue (isLt c) ⇒ ¬ (¬ (istrue (isGt (opp c))))) _ _ _ (x ≐ y)
+  { assume Hbot Hbotbot; refine Hbot }
+  { assume H H2; refine H2 H }
+  { assume Hbot Hbotbot; refine Hbot };
+  assume H1; refine (e H1);
+end;
+
+opaque symbol <_¬_≥ x y : π (x < y ⇒ ¬ (x ≥ y)) ≔
+begin
+  assume x y;
+  assume xLty neg_xLty;
+  refine neg_xLty xLty
+end;
+
+opaque symbol >_¬_≤ x y : π (x > y ⇒ ¬ (x ≤ y)) ≔
+begin
+  assume x y; refine (λ x, x);
+end;
+
 // Compatibility of directional comparison operators
 
 opaque symbol ≤_compat_add x y a : π (x ≤ y ⇒ x + a ≤ y + a) ≔
@@ -592,13 +967,55 @@ begin
   { assume x; assume y f h; apply ⊥ₑ; refine f }
 end;
 
-// Reflexivity
-
 opaque symbol ≤_refl x : π (x ≤ x) ≔
 begin
   assume x; refine ≤_compat_add Z0 Z0 x _; refine (λ x, x);
 end;
 
+opaque symbol ≥_refl x : π (x ≥ x) ≔
+begin
+  assume x; simplify; assume H;
+  have G : π (istrue (isLt Eq)) { rewrite left ≐_refl x; refine H };
+  apply ⊥ₑ G
+end;
+
+opaque symbol ≥_¬_< x y : π (x ≥ y ⇒ ¬ (x < y)) ≔
+begin
+  assume x y; assume H; refine H
+end;
+
+opaque symbol <_irrefl x : π (¬ (x < x)) ≔
+begin
+  assume x;
+  simplify <;
+  refine fold_⇒ _;
+  rewrite ≐_refl;
+  refine (λ x, x);
+end;
+
+opaque symbol >_irrefl x : π (¬ (x > x)) ≔
+begin
+  assume x;
+  simplify >;
+  simplify ≤;
+  refine fold_⇒ _;
+  rewrite ≐_refl;
+  simplify;
+  assume contra;
+  apply contra;
+  refine (λ x, x);
+end;
+
+opaque symbol =_≤ x y : π (x = y ⇒ x ≤ y) ≔
+begin
+  assume x y Heq; rewrite Heq; refine ≤_refl y
+end;
+
+opaque symbol =_≥ x y : π (x = y ⇒ x ≥ y) ≔
+begin
+  assume x y Heq; rewrite Heq; refine ≥_refl y
+end;
+
 // Antisymmetry
 
 opaque symbol ≤_antisym x y : π (x ≤ y ⇒ y ≤ x ⇒ x = y) ≔
@@ -658,51 +1075,249 @@ begin
   refine <_compat_add Z0 (z - x) x;
 end;
 
-// Multiplication
+// Relating the directional comparison operators
 
-symbol * : ℤ → ℤ → ℤ;
-notation * infix right 22;
+opaque symbol ≥_≤ x y : π (x ≥ y ⇔ y ≤ x) ≔
+begin
+  assume x y;
+  apply ∧ᵢ
+  { have e : π (¬ (istrue (isLt (x ≐ y))) ⇒ ¬ (istrue (isGt (y ≐ x))))
+    { rewrite ≐_com y x;
+      refine ind_Comp (λ c, ¬ (istrue (isLt c)) ⇒ ¬ (istrue (isGt (opp c)))) _ _ _ (x ≐ y)
+      { refine (λ x, x) }
+      { assume H1 H2; refine H1 H2 }
+      { refine (λ x, x) } };
+    refine e }
+  { have e : π (¬ (istrue (isGt (y ≐ x))) ⇒ ¬ (istrue (isLt (x ≐ y))))
+    { rewrite ≐_com y x;
+      refine ind_Comp (λ c, ¬ (istrue (isGt (opp c))) ⇒ ¬ (istrue (isLt c))) _ _ _ (x ≐ y)
+      { refine (λ x, x) }
+      { assume H1 H2; refine H1 H2 }
+      { refine (λ x, x) } };
+    refine e };
+end;
 
-rule Z0      * _       ↪ Z0
-with _       * Z0       ↪ Z0
-with Zpos $x * Zpos $y ↪ Zpos (mul $x $y)
-with Zpos $x * Zneg $y ↪ Zneg (mul $x $y)
-with Zneg $x * Zpos $y ↪ Zneg (mul $x $y)
-with Zneg $x * Zneg $y ↪ Zpos (mul $x $y);
+opaque symbol <_> x y : π (x < y ⇔ y > x) ≔
+begin
+  assume x y;
+  apply ∧ᵢ
+  { have e : π (istrue (isLt (x ≐ y)) ⇒ ¬ ¬ istrue (isGt (y ≐ x)))
+    { rewrite ≐_com;
+      refine ind_Comp (λ c, istrue (isLt (opp c)) ⇒ ¬ (¬ (istrue (isGt c)))) _ _ _ (y ≐ x)
+      { assume contra; apply ⊥ₑ contra }
+      { assume contra; apply ⊥ₑ contra }
+      { assume islt ngt; refine ngt islt } };
+    refine e }
+  { have e : π (¬ ¬ istrue (isGt (y ≐ x)) ⇒ istrue (isLt (x ≐ y)))
+    { rewrite ≐_com;
+      refine ind_Comp (λ c, ¬ (¬ (istrue (isGt (opp c)))) ⇒ istrue (isLt c)) _ _ _ (x ≐ y)
+      { assume H; refine H (λ x, x) }
+      { assume H; apply ⊤ᵢ }
+      { assume H; refine H (λ x, x) } };
+    refine e }
+end;
 
-// shortcuts
+opaque symbol >_≥ x y : π (x > y ⇒ x ≥ y) ≔
+begin
+  assume x y;
+  refine ind_Comp (λ c, ¬ (¬ (istrue (isGt c))) ⇒ ¬ istrue (isLt c)) _ _ _ (x ≐ y)
+  { assume H; refine (λ x, x) }
+  { assume H H2; refine H (λ x, x) }
+  { assume H; refine (λ x, x) }
+end;
 
-symbol _1 ≔ Zpos _1;
-symbol _2 ≔ Zpos _2;
-symbol _3 ≔ Zpos _3;
-symbol _4 ≔ Zpos _4;
-symbol _5 ≔ Zpos _5;
-symbol _6 ≔ Zpos _6;
-symbol _7 ≔ Zpos _7;
-symbol _8 ≔ Zpos _8;
-symbol _9 ≔ Zpos _9;
-symbol _10 ≔ Zpos _10;
+opaque symbol ¬_≥_< x y : π (¬ (x ≥ y) ⇒ x < y) ≔
+begin
+  assume x y;
+  simplify;
+  have e : π (¬ ¬ (istrue (isLt (x ≐ y))) ⇒ istrue (isLt (x ≐ y)))
+  { refine ind_Comp (λ c, ¬ ¬ (istrue (isLt c)) ⇒ istrue (isLt c)) _ _ _ (x ≐ y)
+    { assume H; refine H (λ x, x) }
+    { assume H; apply ⊤ᵢ }
+    { assume H; refine H (λ x, x) } };
+  refine e
+end;
 
-// enable printing of integers in decimal notation
+opaque symbol ¬_≤_> x y : π (¬ (x ≤ y) ⇒ x > y) ≔
+begin
+  assume x y; refine (λ x, x)
+end;
 
-builtin "int_zero" ≔ Z0;
-builtin "int_positive" ≔ Zpos;
-builtin "int_negative" ≔ Zneg;
+// Interaction of the comparison operators with the opposite
 
-// enable parsing of integers in decimal notation
+opaque symbol ≤_opp x y : π (x ≥ y ⇔ (— x ≤ — y)) ≔
+begin
+  assume x y;
+  simplify;
+  rewrite ≐_opp x y;
+  apply ∧ᵢ
+  { refine ind_Comp (λ c, (istrue (isLt c) ⇒ ⊥) ⇒ (istrue (isGt (opp c)) ⇒ ⊥)) _ _ _ (x ≐ y)
+    { assume H; refine H }
+    { assume H1 H2; refine H1 H2 }
+    { assume H; refine H } }
+  { refine ind_Comp (λ c, (istrue (isGt (opp c)) ⇒ ⊥) ⇒ (istrue (isLt c) ⇒ ⊥)) _ _ _ (x ≐ y)
+    { assume H; refine H }
+    { assume H1 H2; refine H1 H2 }
+    { assume H; refine H } }
+end;
 
-builtin "0" ≔ Z0;
-builtin "1" ≔ _1;
-builtin "2" ≔ _2;
-builtin "3" ≔ _3;
-builtin "4" ≔ _4;
-builtin "5" ≔ _5;
-builtin "6" ≔ _6;
-builtin "7" ≔ _7;
-builtin "8" ≔ _8;
-builtin "9" ≔ _9;
-builtin "10" ≔ _10;
+opaque symbol <_opp x y : π (x > y ⇔ (— x < — y)) ≔
+begin
+  assume x y;
+  simplify;
+  rewrite ≐_opp x y;
+  apply ∧ᵢ
+  { refine ind_Comp (λ c, ((istrue (isGt c) ⇒ ⊥) ⇒ ⊥) ⇒ istrue (isLt (opp c))) _ _ _ (x ≐ y)
+    { assume H; refine H (λ x, x) }
+    { assume H; refine H (λ x, x) }
+    { assume H; apply ⊤ᵢ } }
+  { refine ind_Comp (λ c, istrue (isLt (opp c)) ⇒ ((istrue (isGt c) ⇒ ⊥) ⇒ ⊥)) _ _ _ (x ≐ y)
+    { assume contra H; apply contra }
+    { assume contra H; apply contra }
+    { assume Hislt Hngt; refine Hngt Hislt } }
+end;
 
-builtin "+" ≔ +;
-builtin "*" ≔ *;
-builtin "-" ≔ —;
+// Comparison with the successor
+
+opaque symbol <_add_Zpos x a : π (x < x + Zpos a) ≔
+begin
+  assume x a;
+  have e : π (x + 0 = x) { refine +Z0 x };
+  rewrite left .[t in t < _] e;
+  rewrite +_com;
+  rewrite +_com x (Zpos a);
+  refine <_compat_add 0 (Zpos a) x _;
+  apply ⊤ᵢ
+end;
+
+opaque symbol ≤_¬_≥_succ t s : π (t ≤ s ⇒ ¬ (t ≥ s + Zpos H)) ≔
+begin
+  assume t s Ht≤s;
+  refine <_¬_≥ t (s + Zpos H) _;
+  refine <_trans_2 t s (s + Zpos H) Ht≤s _;
+  refine <_add_Zpos s H
+end;
+
+// Comparison of a difference with 0
+
+opaque symbol ≥_sub t s : π (t ≥ s ⇒ t - s ≥ 0) ≔
+begin
+  assume t s H;
+  refine ∧ₑ₂ (≥_≤ (t - s) 0) _;
+  have g : π (s ≤ t) { refine ∧ₑ₁ (≥_≤ t s) H };
+  have g2 : π (s + (— s) ≤ t + (— s)) { refine ≤_compat_add s t (— s) g };
+  rewrite left -_same s;
+  refine g2
+end;
+
+opaque symbol sub_≥ t s : π (t - s ≥ 0 ⇒ t ≥ s) ≔
+begin
+  assume t s H;
+  refine ∧ₑ₂ (≥_≤ t s) _;
+  have e : π (0 ≤ t - s) { refine (∧ₑ₁ (≥_≤ (t - s) 0)) H };
+  have H2 : π (0 + s ≤ (t - s) + s) { refine ≤_compat_add 0 (t - s) s e };
+  have H3 : π (0 + s ≤ t) { rewrite left simpl_inv_right t s; refine H2 };
+  refine H3
+end;
+
+opaque symbol >_sub t s : π (t > s ⇒ t - s > 0) ≔
+begin
+  assume t s H;
+  refine ∧ₑ₁ (<_> 0 (t - s)) _;
+  have g : π (s < t) { refine ∧ₑ₂ (<_> s t) H };
+  remove H;
+  have g2 : π (s + (— s) < t + (— s)) { refine <_compat_add s t (— s) g };
+  rewrite left -_same s;
+  refine g2
+end;
+
+opaque symbol sub_> t s : π (t - s > 0 ⇒ t > s) ≔
+begin
+  assume t s H;
+  refine ∧ₑ₁ (<_> s t) _;
+  have e : π (0 < t - s) { refine (∧ₑ₂ (<_> 0 (t - s))) H };
+  have H2 : π (0 + s < (t - s) + s) { refine <_compat_add 0 (t - s) s e };
+  have H3 : π (0 + s < t) { rewrite left simpl_inv_right t s; refine H2 };
+  refine H3
+end;
+
+// Compatibility of comparison with the multiplication
+
+opaque symbol <_compat_mul x y r : π (x < y ⇔ x * Zpos r < y * Zpos r) ≔
+begin
+  assume x y r; simplify; rewrite ≐_compat_mul x y r; refine ⇔_refl
+end;
+
+opaque symbol <_compat_mul_pos p : π (Z0 < p) → Π x y, π (x < y ⇔ x * p < y * p) ≔
+begin
+  induction
+   { assume h x y; refine ⊥ₑ h }
+   { assume r h x y; refine <_compat_mul x y r }
+   { assume r h x y; refine ⊥ₑ h }
+end;
+
+opaque symbol ≤_compat_mul x y r : π (x ≤ y ⇔ x * Zpos r ≤ y * Zpos r) ≔
+begin
+  assume x y r; simplify; rewrite ≐_compat_mul x y r; refine ⇔_refl
+end;
+
+opaque symbol >_compat_mul x y r : π (x > y ⇔ x * Zpos r > y * Zpos r) ≔
+begin
+  assume x y r; simplify; rewrite ≐_compat_mul x y r; refine ⇔_refl
+end;
+
+opaque symbol ≥_compat_mul x y r : π (x ≥ y ⇔ x * Zpos r ≥ y * Zpos r) ≔
+begin
+  assume x y r; simplify; rewrite ≐_compat_mul x y r; refine ⇔_refl
+end;
+
+opaque symbol ≐_mul_opp x y z : π ((x * — z ≐ y * — z) = opp (x * z ≐ y * z)) ≔
+begin
+  assume x y z;
+  rewrite left distr_—_*_r x z;
+  rewrite left distr_—_*_r y z;
+  refine ≐_opp (x * z) (y * z)
+end;
+
+opaque symbol ≐_compat_mul_neg z : π (Z0 < z) → Π x y, π ((y ≐ x) = (x * — z ≐ y * — z)) ≔
+begin
+  induction
+   { assume h x y; refine ⊥ₑ h }
+   { assume r h x y;
+     have e : π ((x * — Zpos r ≐ y * — Zpos r) = opp (x * Zpos r ≐ y * Zpos r))
+     { refine ≐_mul_opp x y (Zpos r) };
+     rewrite e;
+     rewrite left ≐_compat_mul x y r;
+     refine ≐_com y x }
+   { assume r h x y; refine ⊥ₑ h }
+end;
+
+opaque symbol <_compat_mul_neg z : π (Z0 < z) → Π x y, π (x < y ⇔ y * — z < x * — z) ≔
+begin
+  induction
+   { assume h x y; refine ⊥ₑ h }
+   { assume r h x y; simplify;
+     rewrite ≐_compat_mul_neg (Zpos r) ⊤ᵢ y x; refine ⇔_refl }
+   { assume r h x y; refine ⊥ₑ h }
+end;
+
+opaque symbol ≤_compat_mul_neg z : π (Z0 < z) → Π x y, π (x ≤ y ⇔ y * — z ≤ x * — z) ≔
+begin
+  induction
+   { assume h x y; refine ⊥ₑ h }
+   { assume r h x y; simplify;
+     rewrite ≐_compat_mul_neg (Zpos r) ⊤ᵢ y x; refine ⇔_refl }
+   { assume r h x y; refine ⊥ₑ h }
+end;
+
+opaque symbol *_pos x y : π (0 < x ⇒ 0 < y ⇒ 0 < x * y) ≔
+begin
+  induction
+  { assume y h1 h2; refine ⊥ₑ h1 }
+  { assume a;
+    induction
+     { assume h1 h2; refine ⊥ₑ h2 }
+     { assume b h1 h2; refine ⊤ᵢ }
+     { assume b h1 h2; refine ⊥ₑ h2 } }
+  { assume a y h1 h2; refine ⊥ₑ h1 }
+end;