From b5239aae76992ba2360590b5642366aeaad575c0 Mon Sep 17 00:00:00 2001
From: melanie-taprogge <melanie.taprogge@icloud.com>
Date: Mon, 29 Jun 2026 16:30:01 +0200
Subject: [PATCH 1/5] Changed reduction

- removed Rocq incompatible rewrite rules
- fixed proofs
- moved the rules to dedicated file Reduction.lp
---
 Bool.lp      |  24 ++++--
 CHANGES.md   |   5 ++
 List.lp      | 100 ++++++++++++++++---------
 Nat.lp       | 206 +++++++++++++++++++++++++++------------------------
 Pos.lp       | 111 +++++++++++++++++++++------
 Pos_rules.lp |   7 ++
 Reduction.lp |  60 +++++++++++++++
 Z.lp         |  55 +++++++++-----
 8 files changed, 390 insertions(+), 178 deletions(-)
 create mode 100644 Pos_rules.lp
 create mode 100644 Reduction.lp

diff --git a/Bool.lp b/Bool.lp
index 3bb0c70..4e9c67d 100644
--- a/Bool.lp
+++ b/Bool.lp
@@ -111,9 +111,23 @@ symbol or : 𝔹 → 𝔹 → 𝔹;
 notation or infix left 20;
 
 rule true  or _     ↪ true
-with _     or true  ↪ true
-with false or $b    ↪ $b
-with $b    or false ↪ $b;
+with false or $b    ↪ $b;
+
+opaque symbol or_true_lhs [p : 𝔹] : 
+  π ((p or true) = true) ≔
+begin
+  induction
+    {reflexivity}
+    {reflexivity}
+end;
+
+opaque symbol or_false_lhs [p : 𝔹] : 
+  π ((p or false) = p) ≔
+begin
+  induction
+    {reflexivity}
+    {reflexivity}
+end;
 
 opaque symbol ∨_istrue [p q : 𝔹] : π(p or q) → π(p ∨ q) ≔
 begin
@@ -154,8 +168,8 @@ end;
 opaque symbol orC p q : π (p or q = q or p) ≔
 begin
     induction
-    { reflexivity; }
-    { reflexivity; }
+    { assume q; rewrite or_true_lhs [q]; reflexivity }
+    { assume q; rewrite or_false_lhs [q]; reflexivity }
 end;
 
 opaque symbol orA p q r : π ((p or q) or r = p or (q or r)) ≔
diff --git a/CHANGES.md b/CHANGES.md
index 1ce4fce..28af90f 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -15,6 +15,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 
 - definition of Pos.mul
 
+### Changed
+
+- Removed/ changed rewrite rules to match the native Rocq encodings
+- Reintroduced the original rules in Reduction.lp
+
 ## 1.3.1 (2025-11-25)
 
 ### Fixed
diff --git a/List.lp b/List.lp
index c939458..9e245e7 100644
--- a/List.lp
+++ b/List.lp
@@ -403,8 +403,6 @@ begin
     { assume x l' h; simplify; rewrite h; reflexivity; }
 end;
 
-rule $m ++ □ ↪ $m;
-
 opaque symbol size_cat [a] (l m : 𝕃 a) : π(size (l ++ m) = size l + size m) ≔
 begin
   assume a;
@@ -415,8 +413,6 @@ begin
     { assume x l' h m; simplify; rewrite h; reflexivity; }
 end;
 
-rule size ($l ++ $m) ↪ size $l + size $m;
-
 opaque symbol catA  [a] (l m n : 𝕃 a) : π((l ++ m) ++ n = l ++ (m ++ n)) ≔
 begin
   assume a;
@@ -427,8 +423,6 @@ begin
     { assume x l' h m n; simplify; rewrite h; reflexivity; }
 end;
 
-rule ($l ++ $m) ++ $n ↪ $l ++ ($m ++ $n);
-
 opaque symbol cat_nilp [a] (l1 l2 : 𝕃 a) :
   π (nilp (l1 ++ l2) = (nilp l1 and nilp l2)) ≔
 begin
@@ -454,14 +448,14 @@ opaque symbol catrev_cat [a] (l m:𝕃 a): π(catrev l m = rev l ++ m) ≔
 begin
 assume a; induction
 { reflexivity }
-{ assume x l ih m; simplify; rewrite ih; rewrite ih (x ⸬ □); reflexivity }
+{ assume x l ih m; simplify; rewrite ih; rewrite ih (x ⸬ □); rewrite catA; reflexivity }
 end;
 
 opaque symbol rev_cons [a] l (x:τ a): π(rev (x ⸬ l) = rev l ++ (x ⸬ □)) ≔
 begin
   assume a; induction
   { reflexivity }
-  { assume y l ih x; simplify; rewrite catrev_cat; rewrite catrev_cat l (y ⸬ □); reflexivity }
+  { assume y l ih x; simplify; rewrite catrev_cat; rewrite catrev_cat l (y ⸬ □); rewrite catA; reflexivity }
 end;
 
 opaque symbol rev_cat [a] (l m : 𝕃 a) : π(rev (l ++ m) = rev m ++ rev l) ≔
@@ -469,9 +463,9 @@ begin
   assume a;
   induction
     // case l = □
-    { simplify; reflexivity; }
+    { assume l; simplify; rewrite cats0; reflexivity }
     // case l = ⸬
-    { assume x l h m; simplify ++; rewrite rev_cons; rewrite rev_cons; rewrite h; reflexivity; }
+    { assume x l h m; simplify ++; rewrite rev_cons; rewrite rev_cons; rewrite h; rewrite catA; reflexivity; }
 end;
 
 opaque symbol rev_idem [a] (l :𝕃 a) : π(rev (rev l) = l) ≔
@@ -487,7 +481,8 @@ begin
     // case l = □
     { reflexivity }
     // case l = ⸬
-    { assume x l h; rewrite rev_cons; rewrite size_cat; rewrite h; reflexivity }
+    { assume x l h; rewrite rev_cons; rewrite size_cat; rewrite h; simplify; 
+    rewrite suc=+1; rewrite suc=+1; rewrite add0n; reflexivity}
 end;
 
 // rcons
@@ -549,11 +544,20 @@ assert x ⊢ indexes (x ⸬ x ⸬ x  ⸬ x ⸬ □) ≡ 0 ⸬ 1 ⸬ 2 ⸬ 3 ⸬
 symbol last [a] : τ a → 𝕃 a → τ a;
 
 rule last $x □ ↪ $x
-with last _ ($e ⸬ $l) ↪ last $e $l;
+with last _ ($e ⸬ □) ↪ $e
+with last $x (_ ⸬ ($e ⸬ $l)) ↪ last $x ($e ⸬ $l);
 
 assert ⊢ last 4 (3 ⸬ 2 ⸬ 1 ⸬ □) ≡ 1;
 assert ⊢ last 4 □ ≡ 4;
 
+opaque symbol lastl [a : Set] (l : 𝕃 a) (x y : τ a): π ((last x (y ⸬ l)) = last y l)≔
+begin
+  assume a;
+  induction
+    {reflexivity}
+    {assume p l h x y; simplify; rewrite h; rewrite h; reflexivity}
+end;
+
 // belast
 
 symbol belast [a] : τ a → 𝕃 a → 𝕃 a;
@@ -567,7 +571,8 @@ assert ⊢ belast 4 (3 ⸬ 2 ⸬ 1 ⸬ □) ≡ 4 ⸬ 3 ⸬ 2 ⸬ □;
 
 symbol nth [a] : τ a → 𝕃 a → ℕ → τ a;
 
-rule nth $x □ _ ↪ $x
+rule nth $x □ 0 ↪ $x
+with nth $x □ (_ +1) ↪ $x
 with nth _ ($e ⸬ _) 0 ↪ $e
 with nth $x (_ ⸬ $l) ($n +1) ↪ nth $x $l $n;
 
@@ -576,6 +581,13 @@ assert ⊢ nth 4 (3 ⸬ 2 ⸬ 1 ⸬ □) 2 ≡ 1;
 assert ⊢ nth 4 (3 ⸬ 2 ⸬ 1 ⸬ □) 3 ≡ 4;
 assert ⊢ nth 4 (3 ⸬ 2 ⸬ 1 ⸬ □) 42 ≡ 4;
 
+opaque symbol nthx□ [a: Set] n (x : τ a) : π((nth x □ n) = x)≔
+begin
+  assume n; induction
+    {reflexivity}
+    {assume m h x; reflexivity;}
+end;
+
 // set_nth
 
 symbol set_nth [a] : τ a → 𝕃 a → ℕ → τ a → 𝕃 a;
@@ -723,7 +735,7 @@ begin
   assume a b x y; induction
   { assume lb i h;
     have t: π (lb = □) { apply size0nil lb; symmetry; apply h; };
-    rewrite t; reflexivity; }
+    rewrite t; simplify; rewrite nthx□; rewrite nthx□; rewrite nthx□; reflexivity}
   { assume ea la h; induction
     { assume i j; apply ⊥ₑ (s≠0 j); }
     { assume eb lb k; induction
@@ -752,12 +764,20 @@ end;
 symbol drop [a] : ℕ → 𝕃 a → 𝕃 a;
 
 rule drop 0 $l ↪ $l
-with drop _ □ ↪ □
+with drop (_ +1) □ ↪ □
 with drop ($n +1) (_ ⸬ $l) ↪ drop $n $l;
 
 assert ⊢ drop 3 (7 ⸬ 2 ⸬ 3 ⸬ 1 ⸬ 41 ⸬ □) ≡ 1 ⸬ 41 ⸬ □;
 assert ⊢ drop 10 (7 ⸬ 2 ⸬ 3 ⸬ 1 ⸬ 41 ⸬ □) ≡ □;
 
+opaque symbol dropx□ [a: Set] n: π (drop n (□ [a]) = □)≔
+begin
+  assume a;
+  induction
+    {reflexivity}
+    {reflexivity}
+  end;
+
 opaque symbol drop0 [a] (l:𝕃 a) : π (drop 0 l = l) ≔
 begin
   reflexivity;
@@ -792,7 +812,7 @@ end;
 opaque symbol size_drop [a] (l:𝕃 a) n : π (size (drop n l) = size l - n) ≔
 begin
   assume a; induction
-  { reflexivity; }
+  { assume n; rewrite dropx□; reflexivity}
   { assume e l h; simplify; induction
     { reflexivity; }
     { assume n i; simplify; apply h n; } 
@@ -828,10 +848,11 @@ opaque symbol drop_drop [a] (l:𝕃 a) n1 n2 :
   π (drop n1 (drop n2 l) = drop (n1 + n2) l) ≔
 begin
   assume a; induction
-  { reflexivity; }
+  { assume n m; rewrite dropx□; rewrite dropx□; 
+    rewrite dropx□; reflexivity }
   { assume e l h n1; induction
-    { reflexivity; }
-    { assume n2 i; simplify; apply h n1 n2; }
+    { simplify; rewrite addn0; reflexivity; }
+    { assume n2 i; simplify; rewrite addnS; apply h n1 n2; }
   }
 end;
 
@@ -840,12 +861,20 @@ end;
 symbol take [a] : ℕ → 𝕃 a → 𝕃 a;
 
 rule take 0 _ ↪ □
-with take _ □ ↪ □
+with take (_ +1) □ ↪ □
 with take ($n +1) ($x ⸬ $l) ↪ $x ⸬ (take $n $l);
 
 assert ⊢ take 3 (7 ⸬ 2 ⸬ 3 ⸬ 1 ⸬ 41 ⸬ □) ≡ 7 ⸬ 2 ⸬ 3 ⸬ □;
 assert ⊢ take 10 (7 ⸬ 2 ⸬ 3 ⸬ 1 ⸬ 41 ⸬ □) ≡ 7 ⸬ 2 ⸬ 3 ⸬ 1 ⸬ 41 ⸬ □;
 
+opaque symbol taken□ [a: Set] n: π (take n (□ [a]) = □)≔
+begin
+  assume a;
+  induction
+    {reflexivity}
+    {reflexivity}
+  end;
+
 opaque symbol take0 [a] (l: 𝕃 a) : π (take 0 l = □) ≔
 begin
   reflexivity;
@@ -943,10 +972,10 @@ begin
     }
   }
   { assume n h; induction
-    { reflexivity; }
+    { assume l; rewrite addn0; reflexivity }
     { assume m i; induction
       { reflexivity; }
-      { assume e l j; simplify; apply i l; }
+      { assume e l j; simplify; rewrite addnS; apply i l; }
     }
   }
 end;
@@ -957,10 +986,10 @@ begin
   assume a; induction
   { reflexivity; }
   { assume m h; induction
-    { reflexivity; }
+    { assume l; simplify; rewrite addn0; rewrite cats0; reflexivity }
     { assume n i; induction
       { reflexivity; }
-      { assume e l j; simplify; apply feq (λ l:𝕃 a, e ⸬ l);
+      { assume e l j; simplify; apply feq (λ l:𝕃 a, e ⸬ l); rewrite addnS;
         rewrite left addnS; apply h (n +1) l; }
     }
   }
@@ -970,9 +999,9 @@ opaque symbol takeC [a] (l:𝕃 a) i j:
   π (take i (take j l) = take j (take i l)) ≔
 begin
   assume a; induction
-  { reflexivity; }
+  { assume i j; rewrite taken□; rewrite taken□; rewrite taken□; reflexivity}
   { assume e l h; induction
-    { reflexivity; }
+    { assume i; simplify; rewrite taken□; reflexivity }
     { assume i h2; induction
       { reflexivity; }
       { assume j h3; simplify; rewrite h i j; reflexivity; }
@@ -993,12 +1022,12 @@ end;
 
 opaque symbol rot0 [a] (l:𝕃 a) : π (rot 0 l = l) ≔
 begin
-  reflexivity;
+  assume a l; simplify; rewrite cats0; reflexivity
 end;
 
 opaque symbol size_rot [a] (l:𝕃 a) n0 : π (size (rot n0 l) = size l) ≔
 begin
-  assume a l n0; simplify; rewrite addnC;
+  assume a l n0; simplify; rewrite size_cat; rewrite addnC;
   rewrite left @size_cat a (take n0 l) (drop n0 l);
   rewrite cat_take_drop n0 l; reflexivity; 
 end;
@@ -1051,7 +1080,7 @@ end;
 
 opaque symbol rotr0 [a] (l:𝕃 a) : π (rotr 0 l = l) ≔
 begin
-  assume a l; simplify; rewrite take_size l; rewrite @drop_size a; reflexivity;
+  assume a l; simplify; rewrite sub0n; rewrite take_size l; rewrite @drop_size a; reflexivity;
 end;
 
 // membership
@@ -1076,7 +1105,9 @@ end;
 
 opaque symbol mem_seq1 [a] beq (x y:τ a) : π (∈ beq x (y ⸬ □) = beq x y) ≔
 begin
-  assume a beq x y; reflexivity;
+  assume a beq x y; 
+  simplify; rewrite or_false_lhs [beq x y];
+  reflexivity;
 end;
 
 opaque symbol mem_cat [a] beq (x:τ a) l1 l2 :
@@ -1190,7 +1221,8 @@ opaque symbol not_mem_cons_head [a] (beq : τ a → τ a → 𝔹) l l0 x:
 begin
     assume a  beq;
     induction
-        {assume x l0 h; refine h}
+        {assume x l0; simplify ∈; 
+        rewrite or_false_lhs [beq l0 x]; assume h; refine h}
         {assume x l h0 l0 l1 h1 h2;
         have H0 : π ((¬ (istrue (beq l1 l0 or ∈ beq l1 (x ⸬ l)))) ⇒ ⊥)
             {rewrite istrue=true h2; simplify; assume h3; refine h3 ⊤ᵢ};
@@ -1205,7 +1237,7 @@ begin
         {assume x l0 h0 h1; refine h1}
         {assume x l h0 l0 l1 h1 h2;
         have H0 : π ((¬ (istrue (beq l1 l0 or ∈ beq l1 (x ⸬ l)))) ⇒ ⊥)
-            {rewrite istrue=true h2; simplify; assume h3; refine h3 ⊤ᵢ};
+            {rewrite istrue=true h2; rewrite or_true_lhs [beq l1 l0]; simplify; assume h3; refine h3 ⊤ᵢ};
         refine H0 h1}
 end;
 
@@ -1502,7 +1534,7 @@ begin
     refine ind_𝔹 (λ b:𝔹, (filter p (rev l) ++ (if b (e ⸬ □) □) = rev (if b (e ⸬ filter p l) (filter p l)))) _ _ (p e) {
       simplify; rewrite catrev_cat (filter p l) (e ⸬ □); rewrite left h; reflexivity;
     } {
-      simplify; rewrite left rev_def; rewrite h; reflexivity;
+      simplify; rewrite left rev_def; rewrite h; rewrite cats0; reflexivity;
     };
   }
 end;
@@ -1707,7 +1739,7 @@ opaque symbol last_map [a b] (f:τ a → τ b) l x :
 begin
   assume a b f; induction
   { reflexivity; }
-  { assume e l h x; simplify; rewrite h e; reflexivity; }
+  { assume e l h x; simplify; rewrite lastl; rewrite lastl; rewrite h e; reflexivity; }
 end;
 
 opaque symbol belast_map [a b] (f:τ a → τ b) l x :
diff --git a/Nat.lp b/Nat.lp
index 12243a9..06a57ae 100644
--- a/Nat.lp
+++ b/Nat.lp
@@ -196,8 +196,6 @@ begin
   { assume x' h; simplify; rewrite h; reflexivity }
 end;
 
-rule $x + _0 ↪ $x;
-
 opaque symbol addSn x y : π (x +1 + y = (x + y) +1) ≔
 begin
   assume x; reflexivity;
@@ -210,8 +208,6 @@ begin
   { assume x' h y; simplify; rewrite h; reflexivity }
 end;
 
-rule $x + $y +1 ↪ ($x + $y) +1;
-
 opaque symbol add1n n : π ((_0 +1) + n = n +1) ≔
 begin
   assume n; reflexivity;
@@ -219,19 +215,23 @@ end;
 
 opaque symbol addn1 n : π (n + (_0 +1) = n +1) ≔
 begin
-  assume n; reflexivity;
+  assume n; rewrite (addnS n _0); rewrite addn0;
+  reflexivity;
 end;
 
 opaque symbol addSnnS m n : π (m +1 + n = m + n +1) ≔
 begin
-  assume m n; reflexivity;
+  assume m n; rewrite (addnS m n);
+  rewrite addSn m n;
+  reflexivity;
 end;
 
 opaque symbol addnC x y : π (x + y = y + x) ≔
 begin
   induction
-  { reflexivity }
-  { assume x' h y; simplify; rewrite h; reflexivity }
+  { assume y; rewrite addn0; reflexivity }
+  { assume x' h y; simplify; rewrite h; 
+  rewrite addnS (y) (x'); reflexivity }
 end;
 
 opaque symbol addnA x y z : π ((x + y) + z = x + (y + z)) ≔
@@ -241,8 +241,6 @@ begin
   { assume x' h y z; simplify; rewrite h; reflexivity }
 end;
 
-rule ($x + $y) + $z ↪ $x + ($y + $z);
-
 opaque symbol addnCA m n p : π ((m + n) + p = (m + p) + n) ≔
 begin
   assume m n p; symmetry; rewrite addnA; rewrite .[p + n] addnC;
@@ -269,7 +267,7 @@ end;
 
 opaque symbol addnACA m n p q : π ((m + n) + (p + q) = (m + p) + (n + q)) ≔
 begin
-  assume m n p q; simplify; rewrite left .[p + (n + q)] addnA;
+  assume m n p q; rewrite addnA; rewrite addnA; rewrite left .[p + (n + q)] addnA;
   rewrite .[p + n] addnC; rewrite .[(n + p) + q] addnA; reflexivity;
 end;
 
@@ -283,8 +281,9 @@ end;
 opaque symbol addIn x y z : π (x + z = y + z) → π (x = y) ≔
 begin
   assume x y; induction
-  { assume h; apply h;}
-  { assume z h i; apply h; apply +1_inj; apply i;}
+  { rewrite addn0 x; rewrite addn0 y; assume h; apply h;}
+  { assume z h i; apply h; apply +1_inj; 
+  rewrite left addnS x z; rewrite left addnS y z; apply i;}
 end;
 
 opaque symbol addn_eq0 m n : π (m + n = _0 ⇔ m = _0 ∧ n = _0) ≔
@@ -328,7 +327,8 @@ begin
   { assume y h; symmetry; apply 2*=0; symmetry; apply h }
   { assume x h; induction
     { assume i; apply ⊥ₑ (s≠0 i) }
-    { assume y i j; apply feq (+1); apply h; apply +1_inj; apply +1_inj j }
+    { assume y i j; apply feq (+1); apply h; apply +1_inj;
+      rewrite left addnS x x; rewrite left addnS y y; apply +1_inj j }
 }
 end;
 
@@ -337,11 +337,14 @@ begin
   induction
   { induction
     { refine s≠0 }
-    { assume x h; simplify; assume i; apply 0≠s (+1_inj i) }
+    { 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; apply +1_inj; apply +1_inj; apply j }
+    { assume y i j; apply h y; rewrite left addnS x x; apply +1_inj;
+      rewrite left addnS y y; apply +1_inj j }
   }
 end;
 
@@ -350,12 +353,14 @@ end;
 symbol - : ℕ → ℕ → ℕ; notation - infix left 20;
 
 rule _0 - _ ↪ _0
-with $x - _0 ↪ $x
+with $x +1 - _0 ↪ $x +1
 with $x +1 - $y +1 ↪ $x - $y;
 
 opaque symbol sub0n n : π (n - _0 = n) ≔
 begin
-  reflexivity;
+  induction
+    {reflexivity}
+    {assume n h; reflexivity}
 end;
 
 opaque symbol subn0 n : π (_0 - n = _0) ≔
@@ -379,7 +384,7 @@ opaque symbol subn1 n : π (n - (_0 +1) = n ∸1) ≔
 begin
   induction
   { reflexivity }
-  { assume n h; reflexivity;  }
+  { assume n h; simplify; rewrite sub0n; reflexivity;  }
 end;
 
 opaque symbol subnS x y : π (x - (y +1) = (x - y) ∸1) ≔
@@ -387,9 +392,9 @@ begin
   induction
   { reflexivity }
   { assume x h; induction
-    { reflexivity }
+    { simplify; rewrite sub0n; reflexivity }
     { assume y i; simplify; rewrite h; reflexivity }
-  }
+    }
 end;
 
 opaque symbol subSnn n : π (n +1 - n = (_0 +1)) ≔
@@ -404,19 +409,19 @@ begin
   induction
   { reflexivity }
   { assume x h; induction
-    { reflexivity }
+    { simplify; rewrite sub0n; reflexivity }
     { assume y i; simplify; symmetry; rewrite subnS; reflexivity }
-  }
+}
 end;
 
 opaque symbol subnAC z x y : π ((x - y) - z = (x - z) - y) ≔
 begin
   induction
-  { reflexivity }
+  { assume x y; rewrite sub0n; rewrite sub0n; reflexivity }
   { assume z h; induction
     { reflexivity }
     { assume x i; induction
-      { reflexivity }
+      { simplify; rewrite sub0n; reflexivity}
       { assume y j; simplify; rewrite i; rewrite subnS; symmetry;
         rewrite subnS; rewrite predn_sub; reflexivity}
     }
@@ -428,8 +433,8 @@ begin
   induction
   { assume x; simplify; rewrite subnn; reflexivity }
   { assume x h; induction
-    { reflexivity }
-    { simplify; assume y i; rewrite i; reflexivity }
+    { rewrite addn0 (x +1); reflexivity }
+    { simplify; assume y i; rewrite addnS x y; rewrite i; reflexivity }
   }
 end;
 
@@ -440,8 +445,8 @@ begin
   { assume x h; induction
     { reflexivity }
     { assume y i; induction
-      { reflexivity }
-      { assume z j; simplify; rewrite subnS; symmetry; rewrite subnS;
+      { rewrite addn0 (y +1); simplify; rewrite sub0n; reflexivity }
+      { assume z j; simplify; rewrite addnS y z; rewrite subnS; symmetry; rewrite subnS;
         rewrite h; reflexivity }
     }
   }
@@ -452,7 +457,7 @@ begin
   induction
   { assume x y; simplify; reflexivity }
   { assume z h; induction
-    { assume y; simplify; rewrite subnDA; rewrite subnn; reflexivity }
+    { assume y; simplify; rewrite addn0 z; rewrite subnDA; rewrite subnn; reflexivity }
     { assume x i; induction
       { rewrite addnC; rewrite addn0; rewrite addnK; reflexivity }
       { assume y j; rewrite addnC; rewrite subnDA; rewrite addnK; reflexivity }
@@ -485,8 +490,6 @@ begin
   induction { reflexivity } { assume x' h; apply h }
 end;
 
-rule _ * _0 ↪ _0;
-
 opaque symbol muln0 x : π (_0 * x = _0) ≔
 begin
   assume x; reflexivity;
@@ -494,7 +497,7 @@ end;
 
 opaque symbol mul1n n : π ((_0 +1) * n = n) ≔
 begin
-  assume n; reflexivity;
+  assume n; simplify; rewrite addn0 n; reflexivity;
 end;
 
 opaque symbol muln1 n : π (n * (_0 +1) = n) ≔
@@ -521,22 +524,18 @@ begin
   { assume x' h y; simplify; rewrite h; rewrite addnAC; reflexivity }
 end;
 
-//rule $x * ($y +1) ↪ $x + $x * $y; is confluent modulo C only
-
 opaque symbol mulnSr x y : π (x * (y +1) = x * y + x) ≔
 begin
   induction
   { reflexivity }
-  { assume x' h y; simplify; rewrite mulnS; rewrite .[x' + _] addnC;
-    reflexivity }
+  { assume x' h y; simplify; rewrite mulnS; rewrite .[x' + _] addnC; rewrite addnA;
+    rewrite addnS (x' * y) x'; rewrite addnS y ((x' * y) + x'); reflexivity }
 end;
 
-//rule $x * s $y ↪ $x * $y + $x; is confluent modulo C only
-
 opaque symbol mulnC x y : π (x * y = y * x) ≔
 begin
   induction
-  { reflexivity }
+  { assume n; rewrite mul0n; reflexivity }
   { assume x' h y; simplify; rewrite mulnS; rewrite h; reflexivity }
 end;
 
@@ -544,27 +543,23 @@ opaque symbol mulnDl x y z : π ((x + y) * z = x * z + y * z) ≔
 begin
   induction
   { reflexivity }
-  { assume x' h y z; simplify; rewrite h; reflexivity }
+  { assume x' h y z; simplify; rewrite h; rewrite addnA; reflexivity }
 end;
 
-//rule ($x + $y) * $z ↪ $x * $z + $y * $z; is confluent modulo AC only
-
 opaque symbol mulnDr x y z : π (z * (x + y) = z * x + z * y) ≔
 begin
   assume x y z; rewrite mulnC; rewrite mulnDl; rewrite mulnC;
   rewrite .[y * _] mulnC; reflexivity
 end;
 
-//rule $z * ($x + $y) ↪ $z * $x + $z * $y; is confluent modulo AC only
-
 opaque symbol mulnBr x y z : π (x * (y - z) = x * y - x * z) ≔
 begin
   induction
   { reflexivity }
   { assume x h; induction
-    { reflexivity }
+    { assume n; rewrite mul0n; simplify; rewrite mul0n; reflexivity }
     { assume y i; induction
-      { reflexivity }
+      { simplify; rewrite mul0n; rewrite sub0n; reflexivity}
       { assume z j; simplify; rewrite mulnS; rewrite mulnS;
         rewrite left addnAC; rewrite .[z + (x + _)] addnAC;
         rewrite subnDl; rewrite left mulSn; rewrite left mulSn;
@@ -586,8 +581,6 @@ begin
   { assume x' h y z; simplify; rewrite mulnDl; rewrite h; reflexivity }
 end;
 
-//rule ($x * $y) * $z ↪ $x * ($y * $z); is not confluent
-
 opaque symbol mulnCA x y z: π (x * (y * z) = y * (x * z)) ≔
 begin
   assume x y z; rewrite left mulnA; rewrite .[x * y] mulnC; rewrite mulnA;
@@ -621,7 +614,7 @@ begin
     refine ∨ₑ h _ _ {
       assume i; rewrite i; reflexivity;
     } {
-      assume i; rewrite i; reflexivity;
+      assume i; rewrite i; rewrite mul0n; reflexivity;
     };
   };
 end;
@@ -883,7 +876,7 @@ opaque symbol leq_addl m n : π (istrue (n ≤ m + n)) ≔
 begin
   assume m; induction
   { apply ⊤ᵢ }
-  { assume n h; apply h }
+  { assume n h; rewrite addnS m n; apply h }
 end;
 
 opaque symbol leq_addr m n : π (istrue (n ≤ n + m)) ≔
@@ -894,7 +887,7 @@ end;
 opaque symbol leq_subr m n : π (istrue (n - m ≤ n)) ≔
 begin
   induction
-  { assume n; apply ≤_refl n }
+  { assume n; rewrite sub0n; apply ≤_refl n }
   { assume m h; induction
     { apply ⊤ᵢ }
     { assume n i; simplify;
@@ -955,23 +948,20 @@ opaque symbol subn_gt0 m n : π (istrue (_0 < n - m) ⇔ istrue (m < n)) ≔
 begin
   assume m n; apply ∧ᵢ {
     generalize m; induction
-    { assume n h; apply h }
+    { assume n; rewrite sub0n; assume h; apply h }
     { assume m h; induction
       { assume i; apply i }
       { assume n i; rewrite subSS; assume j;
         have t: π (istrue (m < n)) { apply h n j };
-        have u: π (istrue (m +1 < n +1))
-                  { refine ∧ₑ₂ (ltn_add2r (_0 +1) m n) t };
-        rewrite left addn1 m; rewrite left addn1 n; apply u;
+        simplify; apply t;
       }
     }
   } {
     generalize m; induction
-    { assume n h; apply h }
+    { assume n h; rewrite sub0n; apply h }
     { assume m h; induction
       { assume i; apply i }
-      { assume n i j; rewrite subSS; apply h n;
-        refine ∧ₑ₁ (ltn_add2r (_0 +1) m n) j;
+      { assume n i j; rewrite subSS; apply h n; simplify; apply j;
       }
     }
   };
@@ -1004,7 +994,7 @@ end;
 opaque symbol subnKC m n : π (istrue (m ≤ n)) → π (m + (n - m) = n) ≔
 begin
   induction
-  { assume n h; apply eq_refl n }
+  { assume n h; rewrite sub0n; apply eq_refl n }
   { assume m h; induction
     { assume i; apply ⊥ₑ i }
     { assume n i j; apply feq (+1); apply h; apply j }
@@ -1014,10 +1004,10 @@ end;
 opaque symbol addnBn m n : π (m + (n - m) = m - n + n) ≔
 begin
   induction
-  { assume n; apply eq_refl n }
+  { assume n; rewrite sub0n; apply eq_refl n }
   { assume m h; induction
-    { apply eq_refl (m +1) }
-    { assume n i; simplify; apply feq (+1); apply h n }
+    { rewrite subn0 (m +1); rewrite sub0n (m +1); rewrite addn0 (m +1); reflexivity }
+    { assume n i; simplify; rewrite addnS (m - n) n; apply feq (+1); apply h n }
   }
 end;
 
@@ -1064,7 +1054,7 @@ begin
   } {
     assume i;
     have t: π(n - p = _0) { apply ∧ₑ₂ (subn_eq0 n p) i };
-    rewrite t; simplify; apply @leq_trans m n p h i;
+    rewrite t; rewrite addn0 p; apply @leq_trans m n p h i;
   };
 end;
 
@@ -1075,7 +1065,7 @@ begin
   apply ∨ₑ (leq_total p m) {
     assume i;
     have t:π (p - m = _0) { apply (∧ₑ₂ (subn_eq0 p m) i) };
-    rewrite t; simplify; apply @leq_trans p m n i h;
+    rewrite t; rewrite addn0 n; apply @leq_trans p m n i h;
   } {
     assume i; apply ∧ₑ₁ (leq_add2r m p (n + (p - m))) _;
     rewrite addnA; rewrite subnK m p i; rewrite addnC n p;
@@ -1097,13 +1087,20 @@ end;
 symbol max: ℕ → ℕ → ℕ;
 
 rule max _0 $x ↪ $x
-with max $x _0 ↪ $x
+with max ($x +1) _0 ↪ $x +1
 with max ($x +1) ($y +1) ↪ (max $x $y) +1;
 
-opaque symbol maxnC x y : π (max x y = max y x) ≔
+opaque symbol maxn0 x : π (max x _0 = x) ≔
 begin
   induction
   { reflexivity }
+  { reflexivity}
+end;
+
+opaque symbol maxnC x y : π (max x y = max y x) ≔
+begin
+  induction
+  { assume x; rewrite maxn0; reflexivity}
   { assume x h; induction
     { reflexivity }
     { assume y i; simplify; rewrite h; reflexivity }
@@ -1145,8 +1142,9 @@ end;
 opaque symbol addn_maxl x y z: π ((max y z) + x = max (y + x) (z + x)) ≔
 begin
   induction
-  { reflexivity }
-  { assume x h y z; simplify; apply feq (+1); rewrite h; reflexivity;}
+  { assume y z; rewrite addn0 (max y z); rewrite addn0 y; rewrite addn0 z; reflexivity }
+  { assume x h y z; rewrite addnS (max y z) x; rewrite addnS y x; rewrite addnS z x;
+    simplify; apply feq (+1); rewrite h; reflexivity;}
 end;
 
 opaque symbol addn_maxr x y z : π (x + (max y z) = max (x + y) (x + z)) ≔
@@ -1159,9 +1157,9 @@ end;
 opaque symbol subn_maxl x y z: π ( (max x y) - z = max (x - z) (y - z) ) ≔
 begin
   induction
-  { assume y z; reflexivity }
+  { assume y z; simplify; reflexivity }
   { assume x h; induction
-    { assume z; reflexivity }
+    { assume z; rewrite maxn0; simplify; rewrite maxn0; reflexivity}
     { assume y i; induction
       { reflexivity }
       { assume z j; simplify; apply h y z }
@@ -1172,9 +1170,9 @@ end;
 opaque symbol maxnE m n : π (max m n = m + (n - m)) ≔
 begin
   induction
-  { assume n; reflexivity }
+  { assume n; rewrite sub0n; reflexivity }
   { assume m h; induction
-    { simplify;  reflexivity }
+    { simplify; rewrite addn0 m; reflexivity }
     { assume n i; simplify; rewrite h; reflexivity }
   }
 end;
@@ -1186,8 +1184,6 @@ begin
   { assume x h; simplify; rewrite h; reflexivity }
 end;
 
-rule max $x $x ↪ $x;
-
 opaque symbol leq_maxl m n : π (istrue (m ≤ max m n)) ≔
 begin
   induction
@@ -1249,7 +1245,7 @@ begin
     } {
       assume i;
       have t:π (n1 - n2 = _0) { apply ∧ₑ₂ (subn_eq0 n1 n2) i };
-      rewrite t; reflexivity;
+      rewrite t; rewrite mul0n;reflexivity;
     };
   }
 end;
@@ -1391,13 +1387,20 @@ end;
 symbol min : ℕ → ℕ → ℕ;
 
 rule min _0 _ ↪ _0
-with min _ _0 ↪ _0
+with min (_ +1) _0 ↪ _0
 with min ($x +1) ($y +1) ↪ (min $x $y) +1;
 
-opaque symbol minnC x y : π (min x y = min y x) ≔
+opaque symbol minn0 x : π (min x _0 = _0) ≔
 begin
   induction
   { reflexivity }
+  { reflexivity}
+end;
+
+opaque symbol minnC x y : π (min x y = min y x) ≔
+begin
+  induction
+  { assume x; rewrite minn0; reflexivity}
   { assume x h; induction
     { reflexivity }
     { assume y i; simplify; rewrite h; reflexivity }
@@ -1439,8 +1442,9 @@ end;
 opaque symbol addn_minl x y z: π ((min y z) + x = min (y + x) (z + x)) ≔
 begin
   induction
-  { reflexivity }
-  { assume x h y z; simplify; apply feq (+1); rewrite h; reflexivity;}
+  { assume y z; rewrite addn0 (min y z); rewrite addn0 y; rewrite addn0 z; reflexivity }
+  { assume x h y z; rewrite addnS (min y z) x; rewrite addnS y x; rewrite addnS z x;
+    simplify; apply feq (+1); rewrite h; reflexivity;}
 end;
 
 opaque symbol addn_minr x y z: π (x + (min y z) = min (x + y) (x + z)) ≔
@@ -1455,7 +1459,7 @@ begin
   induction
   { assume y z; reflexivity }
   { assume x h; induction
-    { assume z; reflexivity }
+    { assume z; simplify; rewrite minn0; reflexivity }
     { assume y i; induction
       { reflexivity }
       { assume z j; simplify; apply h y z }
@@ -1470,7 +1474,6 @@ begin
   { assume x h; simplify; rewrite h; reflexivity }
 end;
 
-rule min $x $x ↪ $x;
 
 opaque symbol geq_minl m n : π (istrue (min m n ≤ m)) ≔
 begin
@@ -1494,17 +1497,17 @@ begin
   induction
   { assume m; reflexivity }
   { assume m h; induction
-    { reflexivity }
-    { assume n i; simplify; rewrite h n; reflexivity }
+    { rewrite addn0 (m +1); reflexivity }
+    { assume n i; simplify; rewrite addnS (min m n) (max m n);      rewrite addnS m n; rewrite h n; reflexivity }
   }
 end;
 
 opaque symbol maxnK m n : π (min (max m n) m = m) ≔
 begin
   induction
-  { assume n; reflexivity }
+  { assume n; rewrite minn0; reflexivity }
   { assume m h; induction
-    { reflexivity }
+    { simplify; rewrite minnn; reflexivity }
     { assume n i; simplify; rewrite h n; reflexivity }
   }
 end;
@@ -1512,7 +1515,7 @@ end;
 opaque symbol maxKn m n : π (min n (max m n) = n) ≔
 begin
   induction
-  { assume n; reflexivity }
+  { assume n; simplify; rewrite minnn; reflexivity }
   { assume m h; induction
     { reflexivity }
     { assume n i; simplify; rewrite h n; reflexivity }
@@ -1532,7 +1535,7 @@ end;
 opaque symbol minKn m n : π (max n (min m n) = n) ≔
 begin
   induction
-  { assume n; reflexivity }
+  { assume n; simplify; rewrite maxn0; reflexivity }
   { assume m h; induction
     { reflexivity }
     { assume n i; simplify; rewrite h n; reflexivity }
@@ -1555,7 +1558,7 @@ end;
 opaque symbol maxn_minr x y z : π (max (min y z) x = min (max y x) (max z x)) ≔
 begin
   induction
-  { assume y z; reflexivity }
+  { assume y z; rewrite maxn0; rewrite maxn0; rewrite maxn0; reflexivity }
   { assume x h; induction
     { assume z; simplify; rewrite maxKn z (x +1); reflexivity }
     { assume y i; induction
@@ -1581,7 +1584,7 @@ end;
 opaque symbol minn_maxr x y z : π (min (max y z) x = max (min y x) (min z x)) ≔
 begin
   induction
-  { assume y z; reflexivity }
+  { assume y z; rewrite minn0; rewrite minn0; rewrite minn0; reflexivity }
   { assume x h; induction
     { assume z; reflexivity }
     { assume y i; induction
@@ -1594,7 +1597,7 @@ end;
 opaque symbol maxnMr x y z : π ((max y z) * x = max (y * x) (z * x)) ≔
 begin
   induction
-  { assume y z; reflexivity }
+  { assume y z; rewrite mul0n; rewrite mul0n; rewrite mul0n;  reflexivity }
   { assume x h; induction
     { assume z; reflexivity }
     { assume y i; induction
@@ -1615,9 +1618,9 @@ begin
   induction
   { assume y z; reflexivity }
   { assume x h; induction
-    { assume z; reflexivity }
+    { assume z; rewrite mul0n; reflexivity }
     { assume y i; induction
-      { reflexivity }
+      { rewrite mul0n; reflexivity}
       { assume z j; rewrite left addn1 y; rewrite left addn1 z;
         rewrite left addn_maxl (_0 +1) y z; symmetry;
         rewrite mulnDr y (_0 +1) (x +1); rewrite mulnDr z (_0 +1) (x +1);
@@ -1632,7 +1635,7 @@ end;
 opaque symbol minnMr x y z : π ((min y z) * x = min (y * x) (z * x)) ≔
 begin
   induction
-  { assume y z; reflexivity }
+  { assume y z; rewrite mul0n; rewrite mul0n; reflexivity }
   { assume x h; induction
     { assume z; reflexivity }
     { assume y i; induction
@@ -1653,9 +1656,9 @@ begin
   induction
   { assume y z; reflexivity }
   { assume x h; induction
-    { assume z; reflexivity }
+    { assume z; rewrite mul0n; simplify; rewrite mul0n; reflexivity }
     { assume y i; induction
-      { reflexivity }
+      { rewrite mul0n; simplify; rewrite mul0n; reflexivity }
       { assume z j; rewrite left addn1 y; rewrite left addn1 z;
         rewrite left addn_minl (_0 +1) y z; symmetry;
         rewrite mulnDr y (_0 +1) (x +1); rewrite mulnDr z (_0 +1) (x +1);
@@ -1681,7 +1684,7 @@ end;
 
 opaque symbol expn m : π (m ^ (_0 +1) = m) ≔
 begin
-  assume m; simplify; rewrite mulnS; reflexivity;
+  assume m; simplify; rewrite mulnS; rewrite mul0n m; rewrite addn0 m; reflexivity;
 end;
 
 opaque symbol expnS a n : π (a ^ (n +1) = a * a ^ n ) ≔
@@ -1713,7 +1716,7 @@ end;
 opaque symbol expnD a m n: π (a ^ (m + n) = a ^ m * a ^ n) ≔
 begin
   assume a; induction
-  { reflexivity }
+  { assume n; rewrite add0n n; rewrite expn0 a; rewrite mul1n (a ^ n); reflexivity }
   { assume m h n; simplify; rewrite h n; rewrite mulnA; reflexivity }
 end;
 
@@ -1796,6 +1799,13 @@ symbol _8 ≔ _7 +1;
 symbol _9 ≔ _8 +1;
 symbol _10 ≔ _9 +1;
 
+opaque symbol suc=+1 x : π ((x +1) = (x + _1))≔
+begin 
+  induction
+    {reflexivity}
+    {assume n h; rewrite h; rewrite left addSn; rewrite h; reflexivity;}
+end;
+
 // enable parsing of natural numbers in decimal notation
 
 builtin "0"  ≔ _0;
diff --git a/Pos.lp b/Pos.lp
index 89b7294..d177814 100644
--- a/Pos.lp
+++ b/Pos.lp
@@ -105,7 +105,7 @@ assert ⊢ val (O (I H)) ≡ 6;
 opaque opaque symbol valS x : π(val (succ x) = val x +1) ≔
 begin
   induction
-  { assume x h; simplify; rewrite h; reflexivity }
+  { assume x h; simplify; rewrite h; simplify; rewrite addn0; rewrite addnS; reflexivity}
   { assume x h; reflexivity }
   { reflexivity }
 end;
@@ -125,8 +125,11 @@ opaque opaque symbol val≠0 x : π(val x ≠ 0) ≔
 begin
   induction
   { assume x h; refine s≠0 }
-  { assume x h; simplify; assume i;
-    apply h (∧ₑ₁ (∧ₑ₁ (addn_eq0 (val x) (val x)) i))
+  { assume x h; simplify; assume i; 
+    have i' :  π ((val x + (val x)) = 0)
+      {rewrite left .[x in ((_ + x) = _)] addn0 (val x);
+      refine i};
+    apply h (∧ₑ₁ (∧ₑ₁ (addn_eq0 (val x) (val x)) i'))
   }
   { refine s≠0 }
 end;
@@ -141,22 +144,46 @@ begin
   induction
   { assume x h; induction
     { simplify; assume y i j; rewrite h y _
-        { apply 2*_inj; apply +1_inj; apply j }
+        { apply 2*_inj; apply +1_inj; 
+          have j' : π ((((val x + (val x + 0)) +1) = ((val y + (val y + 0)) +1)) ⇒ (((val x + val x) +1) = ((val y + val y) +1)))
+            {rewrite addn0; rewrite addn0; assume h0; refine h0};
+        apply (j' j) }
         { reflexivity }
     }
-    { simplify; assume y i j; apply ⊥ₑ; apply odd≠even (val x) (val y) j }
-    { simplify; assume i; apply ⊥ₑ; apply 2*val≠0 x; apply +1_inj; apply i }
+    { 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) }
+    { 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};
+    apply (H i) }
   }
   { assume x h; induction
     { simplify; assume y i j; apply ⊥ₑ;
-      apply odd≠even (val y) (val x) (eq_sym j) }
-    { simplify; assume y i j; apply feq O; apply h; apply 2*_inj; apply j }
-    { assume i; apply ⊥ₑ; apply odd≠even 0 (val x); symmetry; apply i }
+    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)) }
+    { 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; 
+      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)
+    }
   }
   { induction
     { simplify; assume x h i; apply ⊥ₑ; apply val≠0 x; apply 2*=0; apply +1_inj;
-      symmetry; apply i }
-    { simplify; assume x h i; apply ⊥ₑ; apply odd≠even 0 (val x); apply i }
+      symmetry; 
+      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; 
+      have H: π ((1 = (val x + (val x + 0))) ⇒ (1 = (val x + val x)))
+        {rewrite addn0; assume h0; refine h0};
+    apply (H i) }
     { reflexivity }
   }
 end;
@@ -196,16 +223,53 @@ rule add (I $x) (I $q) ↪ O (add_carry $x $q)
 with add (I $x) (O $q) ↪ I (add $x $q)
 with add (O $x) (I $q) ↪ I (add $x $q)
 with add (O $x) (O $q) ↪ O (add $x $q)
-with add $x      H      ↪ succ $x
-with add H      $y      ↪ succ $y;
+with add (I $x) H      ↪ O (succ $x)
+with add (O $x) H      ↪ I $x
+with add H      (I $q) ↪ O (succ $q)
+with add H      (O $q) ↪ I $q
+with add H      H      ↪ O H;
+
+opaque symbol addnH n : π (add n H = succ n)≔
+begin
+  induction
+    {reflexivity}
+    {reflexivity}
+    {reflexivity}
+end;
+
+opaque symbol addHn n : π (add H n = succ n)≔
+begin
+  induction
+    {reflexivity}
+    {reflexivity}
+    {reflexivity}
+end;
 
 rule add_carry (I $x) (I $q) ↪ I (add_carry $x $q)
 with add_carry (I $x) (O $q) ↪ O (add_carry $x $q)
 with add_carry (O $x) (I $q) ↪ O (add_carry $x $q)
 with add_carry (O $x) (O $q) ↪ I (add $x $q)
-with add_carry $x      H      ↪ add $x (O H)
-with add_carry H      $y      ↪ add (O H) $y;
-// for efficiency reasons last cases should not be 'succ (succ $x)'
+with add_carry (I $x) H      ↪ I (succ $x)
+with add_carry (O $x) H      ↪ O (succ $x)
+with add_carry H      (I $q) ↪ I (succ $q)
+with add_carry H      (O $q) ↪ O (succ $q)
+with add_carry H      H      ↪ I H;
+
+opaque symbol add_carryH n : π (add_carry n H = add n (O H))≔
+begin
+  induction
+    {assume n h; simplify; rewrite addnH; reflexivity }
+    {assume n h; simplify; rewrite addnH; reflexivity }
+    {reflexivity}
+end;
+
+opaque symbol add_carryHn n : π (add_carry H n = add (O H) n)≔
+begin
+  induction
+    {assume n h; simplify; rewrite addHn; reflexivity }
+    {assume n h; simplify; rewrite addHn; reflexivity }
+    {reflexivity}
+end;
 
 // Check that 7 + 5 = 12
 assert ⊢ add (I (I H)) (I (O H)) ≡ O (O (I H));
@@ -224,7 +288,7 @@ begin
     induction
       { reflexivity }
       { assume q h; simplify; rewrite prec; reflexivity }
-      { reflexivity } }
+      { rewrite addnH;  simplify; reflexivity } }
   // case O
   { assume p prec;
     induction
@@ -251,14 +315,17 @@ begin
       { reflexivity }
       { reflexivity } }
   // case H
-  { induction { reflexivity } { reflexivity } { reflexivity } }
+  { induction 
+    { assume q h; simplify; rewrite addHn; reflexivity }
+    { assume q h; simplify; rewrite addHn; reflexivity } 
+    { reflexivity } }
 end;
 
 opaque symbol add_succ_right x y : π (add x (succ y) = succ (add x y)) ≔
 begin
   refine ind_ℙeano (λ x, `∀ y, add x (succ y) = succ (add x y)) _ _
   // case H
-  { reflexivity }
+  { assume n; rewrite addHn; rewrite addHn; reflexivity }
   // case succ
   { assume x xrec y;
     rewrite add_succ; rewrite add_succ; rewrite xrec; reflexivity }
@@ -270,7 +337,7 @@ opaque symbol add_assoc x y z : π (add (add x y) z = add x (add y z)) ≔
 begin
   refine ind_ℙeano (λ x, `∀ y, `∀ z, add (add x y) z = add x (add y z)) _ _
   // case H
-  { refine add_succ }
+  { assume m n; rewrite addHn; rewrite addHn; refine add_succ m n }
   // case succ
   { assume x xrec y z;
     rewrite add_succ; rewrite add_succ; rewrite add_succ;
@@ -283,7 +350,7 @@ opaque symbol add_com x y : π (add x y = add y x) ≔
 begin
   refine ind_ℙeano (λ x, `∀ y, add x y = add y x) _ _
   // case H
-  { reflexivity }
+  { assume n; rewrite addHn; rewrite addnH; reflexivity}
   // case succ
   { assume x xrec y;
     rewrite add_succ; rewrite add_succ_right; rewrite xrec; reflexivity }
@@ -546,7 +613,7 @@ opaque symbol compare_compat_add a x y :
 begin
   refine ind_ℙeano (λ a, `∀ x, `∀ y, compare (add x a) (add y a) = compare x y) _ _
   // case H
-  { assume x y; refine compare_succ_succ x y Eq }
+  { assume x y; rewrite addnH; rewrite addnH; refine compare_succ_succ x y Eq }
   // case succ
   { assume a arec x y;
     rewrite add_succ_right; rewrite add_succ_right; rewrite left arec x y;
diff --git a/Pos_rules.lp b/Pos_rules.lp
new file mode 100644
index 0000000..f61a3ee
--- /dev/null
+++ b/Pos_rules.lp
@@ -0,0 +1,7 @@
+require open Stdlib.Pos;
+
+rule add $x      H      ↪ succ $x
+with add H      $y      ↪ succ $y;
+
+rule add_carry $x      H      ↪ add $x (O H)
+with add_carry H      $y      ↪ add (O H) $y;
\ No newline at end of file
diff --git a/Reduction.lp b/Reduction.lp
new file mode 100644
index 0000000..0d29177
--- /dev/null
+++ b/Reduction.lp
@@ -0,0 +1,60 @@
+/* Reduction rules 
+The rules given here all correspond to proved equalities in their corresponding file.
+They were removed to increase the compatibility with native Rocq encodings. 
+*/
+
+// Rules from Bool.lp
+
+require Stdlib.Bool as B;
+
+rule _ B.or B.true  ↪ B.true
+with $b B.or B.false ↪ $b;
+
+// Rules for Nat.lp
+
+require Stdlib.Nat as N;
+
+rule $x N.+ N._0 ↪ $x;
+
+rule $x N.+ $y N.+1 ↪ ($x N.+ $y) N.+1;
+
+rule ($x N.+ $y) N.+ $z ↪ $x N.+ ($y N.+ $z);
+
+rule $x N.- N._0 ↪ $x;
+
+rule _ N.* N._0 ↪ N._0;
+
+rule N.max $x N._0 ↪ $x;
+
+rule N.max $x $x ↪ $x;
+
+rule N.min _ N._0 ↪ N._0;
+
+rule N.min $x $x ↪ $x;
+
+
+// Rules for List.lp
+
+require Stdlib.List as L;
+
+rule $m L.++ L.□ ↪ $m;
+
+rule L.size ($l L.++ $m) ↪ L.size $l N.+ L.size $m;
+
+rule ($l L.++ $m) L.++ $n ↪ $l L.++ ($m L.++ $n);
+
+rule L.last _ ($e L.⸬ $l) ↪ L.last $e $l;
+
+rule L.nth $x L.□ _ ↪ $x;
+
+rule L.drop _ L.□ ↪ L.□;
+
+rule L.take _ L.□ ↪ L.□;
+
+
+// Rules for Z.lp
+
+require Stdlib.Z as Z;
+
+rule $x Z.+ Z.0 ↪ $x;
+
diff --git a/Z.lp b/Z.lp
index 74cf688..d23f52f 100644
--- a/Z.lp
+++ b/Z.lp
@@ -150,12 +150,21 @@ symbol + : ℤ → ℤ → ℤ;
 notation + infix right 20;
 
 rule Z0      + $y      ↪ $y
-with $x      + Z0      ↪ $x
+with Zpos $x + Z0      ↪ Zpos $x
+with Zneg $x + Z0      ↪ Zneg $x
 with Zpos $x + Zpos $y ↪ Zpos (add $x $y)
 with Zpos $x + Zneg $y ↪ sub $x $y
 with Zneg $x + Zpos $y ↪ sub $y $x
 with Zneg $x + Zneg $y ↪ Zneg (add $x $y);
 
+opaque symbol +Z0 x : π ((x + Z0) = x)≔
+begin
+  induction
+    {reflexivity}
+    {reflexivity}
+    {reflexivity} 
+end;
+
 // Interaction of addition with opposite
 
 opaque symbol distr_—_+ x y : π (— (x + y) = — x + — y) ≔
@@ -204,7 +213,7 @@ opaque symbol pred_double_succ x : π (pred_double (x + Zpos H) = succ_double x)
 begin
   induction
    { reflexivity }
-   { assume x; simplify; rewrite pos_pred_double_succ; reflexivity }
+   { assume x; simplify; rewrite addnH; rewrite pos_pred_double_succ; reflexivity }
    { induction { reflexivity } { reflexivity } { reflexivity } }
 end;
 
@@ -212,7 +221,7 @@ opaque symbol succ_pred_double x : π (pred_double x + Zpos H = double x) ≔
 begin
   induction
    { reflexivity }
-   { assume x; simplify; rewrite succ_pos_pred_double; reflexivity }
+   { assume x; simplify; rewrite addnH; rewrite succ_pos_pred_double; reflexivity }
    { reflexivity }
 end;
 
@@ -225,7 +234,7 @@ opaque symbol double_succ x : π (double (x + Zpos H) = succ_double x + Zpos H)
 begin
   induction
    { reflexivity }
-   { reflexivity }
+   { assume n; simplify; rewrite addnH; reflexivity }
    { induction { reflexivity } { reflexivity } { reflexivity } }
 end;
 
@@ -260,7 +269,7 @@ begin
     induction
       { assume y h; simplify; rewrite left succ_pred_double; reflexivity }
       { assume y h; simplify; rewrite succ_double_carac; reflexivity }
-      { simplify; rewrite succ_pos_pred_double; reflexivity } }
+      { simplify; rewrite addnH; rewrite succ_pos_pred_double; reflexivity } }
   // case H
   { induction
      { induction { reflexivity } { reflexivity } { reflexivity } }
@@ -271,8 +280,8 @@ end;
 opaque symbol add_Zpos_succ x p : π (x + Zpos (succ p) = (x + Zpos p) + Zpos H) ≔
 begin
   induction
-   { reflexivity }
-   { assume x p; simplify; rewrite add_succ_right; reflexivity }
+   { assume n; simplify; rewrite addnH; reflexivity}
+   { assume x p; simplify; rewrite add_succ_right; rewrite addnH; reflexivity }
    { assume x p; simplify; rewrite sub_succ; reflexivity }
 end;
 
@@ -281,7 +290,7 @@ begin
   assume a b c;
   refine ind_ℙeano (λ c, sub a b + Zpos c = sub (add a c) b) _ _ c
   // case H
-  { simplify; rewrite sub_succ; reflexivity }
+  { simplify; rewrite addnH; rewrite sub_succ; reflexivity }
   // case succ
   { assume r rrec; rewrite add_Zpos_succ; rewrite rrec;
     rewrite add_succ_right; rewrite sub_succ; reflexivity }
@@ -313,7 +322,7 @@ begin
 
      { assume y;
        induction
-         { reflexivity }
+         { rewrite +Z0; rewrite +Z0; reflexivity}
          // case Zpos - Zneg - Zpos
          { assume z; simplify; rewrite sub_add_Zpos; rewrite +_com;
            rewrite sub_add_Zpos; rewrite add_com; reflexivity }
@@ -325,7 +334,7 @@ begin
       { reflexivity }
       { assume y;
         induction
-          { reflexivity }
+          { simplify; rewrite +Z0; reflexivity }
           // case Zneg - Zpos - Zpos
           { assume z; simplify; rewrite sub_add_Zpos; reflexivity }
           // case Zneg - Zpos - Zneg
@@ -356,7 +365,12 @@ with Zpos $p ≐ Zpos $q ↪ compare $p $q
 with Zpos _  ≐ Zneg _  ↪ Gt
 with Zneg _  ≐ Z0      ↪ Lt
 with Zneg _  ≐ Zpos _  ↪ Lt
-with Zneg $p ≐ Zneg $q ↪ compare $q $p;
+with Zneg $p ≐ Zneg $q ↪ opp (compare $p $q);
+
+symbol Zneg≐ p q : π ((Zneg p ≐ Zneg q) = compare q p)≔
+begin
+  assume p q; rewrite compare_com; reflexivity
+end;
 
 // ≐ decides the equality of integers
 
@@ -379,7 +393,10 @@ begin
     induction
      { assume H; apply ⊥ₑ; refine Lt≠Eq H }
      { assume y H; apply ⊥ₑ; refine Lt≠Eq H }
-     { assume y H; rewrite compare_decides y x H; reflexivity } }
+     { assume y H;
+       have H' : π (compare y x = Eq)
+       { refine ind_eq (eq_sym (Zneg≐ x y)) (λ c, c = Eq) H };
+       rewrite compare_decides y x H'; reflexivity } }
 end;
 
 // Commutative properties of ≐
@@ -419,7 +436,7 @@ begin
     induction
       { reflexivity }
       { reflexivity }
-      { assume y; simplify; rewrite compare_acc_com; reflexivity } }
+      { assume y; simplify; rewrite opp_idem; reflexivity } }
 end;
 
 // General results
@@ -427,13 +444,13 @@ end;
 opaque symbol simpl_right x a : π ((x + a) - a = x) ≔
 begin
   assume x a; simplify; rewrite +_assoc;
-  rewrite -_same; reflexivity;
+  rewrite -_same; rewrite +Z0; reflexivity;
 end;
 
 opaque symbol simpl_inv_right x a : π ((x - a) + a = x) ≔
 begin
   assume x a; simplify; rewrite +_assoc;
-  rewrite .[— a + a] +_com; rewrite -_same; reflexivity;
+  rewrite .[— a + a] +_com; rewrite -_same; rewrite +Z0; reflexivity;
 end;
 
 // ≐ with 0
@@ -492,7 +509,7 @@ begin
     induction
      { reflexivity }
      { reflexivity }
-     { assume y; simplify; rewrite ≐_pos_sub; reflexivity } }
+     { assume y; simplify; rewrite ≐_pos_sub; rewrite compare_com; reflexivity } }
 end;
 
 // Compatibility of comparison with the addition
@@ -539,7 +556,7 @@ begin
   rewrite .[y + a] +_com; rewrite distr_—_+;
   rewrite left +_assoc a (— a) (— y); rewrite -_same;
   rewrite left +_assoc x Z0 (— y); simplify; refine fold_⇒ _;
-  rewrite left ≐_sub x y; refine H;
+  rewrite +Z0; rewrite left ≐_sub x y; refine H;
 end;
 
 opaque symbol <_compat_add x y a : π (x < y ⇒ x + a < y + a) ≔
@@ -547,8 +564,8 @@ begin
   assume x y a; simplify; assume H; rewrite ≐_sub;
   rewrite +_assoc; rewrite .[y + a] +_com;
   rewrite distr_—_+; rewrite left +_assoc a (— a) (— y);
-  rewrite -_same; rewrite left +_assoc;
-  simplify; rewrite left ≐_sub; refine H;
+  rewrite -_same; rewrite left +_assoc; rewrite +Z0; 
+  rewrite left ≐_sub; refine H;
 end;
 
 opaque symbol ≤_compat_≤ x y : π (Z0 ≤ x ⇒ Z0 ≤ y ⇒ Z0 ≤ x + y) ≔

From b588b144e009edf19fac3314867e02253562c8b1 Mon Sep 17 00:00:00 2001
From: melanie-taprogge <melanie.taprogge@icloud.com>
Date: Mon, 29 Jun 2026 16:58:30 +0200
Subject: [PATCH 2/5] fixes

---
 Pos_rules.lp |  7 -------
 Reduction.lp | 20 +++++++++++++-------
 2 files changed, 13 insertions(+), 14 deletions(-)
 delete mode 100644 Pos_rules.lp

diff --git a/Pos_rules.lp b/Pos_rules.lp
deleted file mode 100644
index f61a3ee..0000000
--- a/Pos_rules.lp
+++ /dev/null
@@ -1,7 +0,0 @@
-require open Stdlib.Pos;
-
-rule add $x      H      ↪ succ $x
-with add H      $y      ↪ succ $y;
-
-rule add_carry $x      H      ↪ add $x (O H)
-with add_carry H      $y      ↪ add (O H) $y;
\ No newline at end of file
diff --git a/Reduction.lp b/Reduction.lp
index 0d29177..0af3500 100644
--- a/Reduction.lp
+++ b/Reduction.lp
@@ -6,14 +6,16 @@ They were removed to increase the compatibility with native Rocq encodings.
 // Rules from Bool.lp
 
 require Stdlib.Bool as B;
+require Stdlib.Nat as N;
+require Stdlib.List as L;
+require Stdlib.Pos as P;
+require Stdlib.Z as Z;
 
 rule _ B.or B.true  ↪ B.true
 with $b B.or B.false ↪ $b;
 
 // Rules for Nat.lp
 
-require Stdlib.Nat as N;
-
 rule $x N.+ N._0 ↪ $x;
 
 rule $x N.+ $y N.+1 ↪ ($x N.+ $y) N.+1;
@@ -35,8 +37,6 @@ rule N.min $x $x ↪ $x;
 
 // Rules for List.lp
 
-require Stdlib.List as L;
-
 rule $m L.++ L.□ ↪ $m;
 
 rule L.size ($l L.++ $m) ↪ L.size $l N.+ L.size $m;
@@ -52,9 +52,15 @@ rule L.drop _ L.□ ↪ L.□;
 rule L.take _ L.□ ↪ L.□;
 
 
-// Rules for Z.lp
+// Rules for Pos.lp
 
-require Stdlib.Z as Z;
+rule P.add $x P.H ↪ P.succ $x
+with P.add P.H $y ↪ P.succ $y;
 
-rule $x Z.+ Z.0 ↪ $x;
+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;
+
+
+// Rules for Z.lp
 
+rule $x Z.+ Z.Z0 ↪ $x;

From a3448816a63c6e4df86587d8caa72b2bddefe5c4 Mon Sep 17 00:00:00 2001
From: melanie-taprogge <melanie.taprogge@icloud.com>
Date: Tue, 30 Jun 2026 10:53:01 +0200
Subject: [PATCH 3/5] cosmetic fixes

---
 Reduction.lp | 6 ++++--
 Z.lp         | 4 ++--
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/Reduction.lp b/Reduction.lp
index 0af3500..a4add08 100644
--- a/Reduction.lp
+++ b/Reduction.lp
@@ -3,17 +3,19 @@ The rules given here all correspond to proved equalities in their corresponding
 They were removed to increase the compatibility with native Rocq encodings. 
 */
 
-// Rules from Bool.lp
-
 require Stdlib.Bool as B;
 require Stdlib.Nat as N;
 require Stdlib.List as L;
 require Stdlib.Pos as P;
 require Stdlib.Z as Z;
 
+
+// Rules from Bool.lp
+
 rule _ B.or B.true  ↪ B.true
 with $b B.or B.false ↪ $b;
 
+
 // Rules for Nat.lp
 
 rule $x N.+ N._0 ↪ $x;
diff --git a/Z.lp b/Z.lp
index d23f52f..1329265 100644
--- a/Z.lp
+++ b/Z.lp
@@ -157,7 +157,7 @@ with Zpos $x + Zneg $y ↪ sub $x $y
 with Zneg $x + Zpos $y ↪ sub $y $x
 with Zneg $x + Zneg $y ↪ Zneg (add $x $y);
 
-opaque symbol +Z0 x : π ((x + Z0) = x)≔
+opaque symbol +Z0 x : π (x + Z0 = x) ≔
 begin
   induction
     {reflexivity}
@@ -367,7 +367,7 @@ with Zneg _  ≐ Z0      ↪ Lt
 with Zneg _  ≐ Zpos _  ↪ Lt
 with Zneg $p ≐ Zneg $q ↪ opp (compare $p $q);
 
-symbol Zneg≐ p q : π ((Zneg p ≐ Zneg q) = compare q p)≔
+symbol Zneg≐ p q : π ((Zneg p ≐ Zneg q) = compare q p) ≔
 begin
   assume p q; rewrite compare_com; reflexivity
 end;

From f1dc383c79b29c6daead0d1890aa9871fe671ec1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Wed, 8 Jul 2026 11:01:33 +0200
Subject: [PATCH 4/5] rename Reduction to ExtraRules, and update CHANGES.md

---
 CHANGES.md                    | 12 +++++++-----
 Reduction.lp => ExtraRules.lp |  0
 2 files changed, 7 insertions(+), 5 deletions(-)
 rename Reduction.lp => ExtraRules.lp (100%)

diff --git a/CHANGES.md b/CHANGES.md
index 35e6915..14f115a 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -3,6 +3,13 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/),
 and this project adheres to [Semantic Versioning](https://semver.org/).
 
+## Unreleased
+
+### Changed
+
+- Changed rewrite rules to be in line with the Rocq standard library.
+- Moved rules not in line with Rocq to the module ExtraRules.
+
 ## 1.4.0 (2026-07-07)
 
 ### Added
@@ -15,11 +22,6 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 
 - definition of Pos.mul
 
-### Changed
-
-- Removed/ changed rewrite rules to match the native Rocq encodings
-- Reintroduced the original rules in Reduction.lp
-
 ## 1.3.1 (2025-11-25)
 
 ### Fixed
diff --git a/Reduction.lp b/ExtraRules.lp
similarity index 100%
rename from Reduction.lp
rename to ExtraRules.lp

From ca4342a0f4cf7da1319931dbe507e1198ce167f8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Wed, 8 Jul 2026 11:08:30 +0200
Subject: [PATCH 5/5] details

---
 ExtraRules.lp | 57 +++++++++++++++------------------------------------
 1 file changed, 17 insertions(+), 40 deletions(-)

diff --git a/ExtraRules.lp b/ExtraRules.lp
index a4add08..ce9aa22 100644
--- a/ExtraRules.lp
+++ b/ExtraRules.lp
@@ -1,68 +1,45 @@
-/* Reduction rules 
-The rules given here all correspond to proved equalities in their corresponding file.
-They were removed to increase the compatibility with native Rocq encodings. 
-*/
+// This module turns proved equalities to rewrite rules
 
-require Stdlib.Bool as B;
+require open Stdlib.Bool;
 require Stdlib.Nat as N;
-require Stdlib.List as L;
+require open Stdlib.List;
 require Stdlib.Pos as P;
 require Stdlib.Z as Z;
 
+// Bool
 
-// Rules from Bool.lp
+rule _ or true  ↪ true
+with $b or false ↪ $b;
 
-rule _ B.or B.true  ↪ B.true
-with $b B.or B.false ↪ $b;
-
-
-// Rules for Nat.lp
+// Nat
 
 rule $x N.+ N._0 ↪ $x;
-
 rule $x N.+ $y N.+1 ↪ ($x N.+ $y) N.+1;
-
 rule ($x N.+ $y) N.+ $z ↪ $x N.+ ($y N.+ $z);
-
 rule $x N.- N._0 ↪ $x;
-
 rule _ N.* N._0 ↪ N._0;
-
 rule N.max $x N._0 ↪ $x;
-
 rule N.max $x $x ↪ $x;
-
 rule N.min _ N._0 ↪ N._0;
-
 rule N.min $x $x ↪ $x;
 
+// List
 
-// Rules for List.lp
+rule $m ++ □ ↪ $m;
+rule size ($l ++ $m) ↪ size $l N.+ size $m;
+rule ($l ++ $m) ++ $n ↪ $l ++ ($m ++ $n);
+rule last _ ($e ⸬ $l) ↪ last $e $l;
+rule nth $x □ _ ↪ $x;
+rule drop _ □ ↪ □;
+rule take _ □ ↪ □;
 
-rule $m L.++ L.□ ↪ $m;
-
-rule L.size ($l L.++ $m) ↪ L.size $l N.+ L.size $m;
-
-rule ($l L.++ $m) L.++ $n ↪ $l L.++ ($m L.++ $n);
-
-rule L.last _ ($e L.⸬ $l) ↪ L.last $e $l;
-
-rule L.nth $x L.□ _ ↪ $x;
-
-rule L.drop _ L.□ ↪ L.□;
-
-rule L.take _ L.□ ↪ L.□;
-
-
-// Rules for Pos.lp
+// Pos
 
 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;
 
-
-// Rules for Z.lp
+// Z
 
 rule $x Z.+ Z.Z0 ↪ $x;