From 42bb5ad6b35ec36822a0700c09ec5f2556b3435a Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sun, 3 Mar 2024 09:55:57 +0000
Subject: [PATCH 1/6] removed extra space

---
 src/Data/Integer/Divisibility.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Integer/Divisibility.agda b/src/Data/Integer/Divisibility.agda
index 28963c8d24..7cd8109fce 100644
--- a/src/Data/Integer/Divisibility.agda
+++ b/src/Data/Integer/Divisibility.agda
@@ -27,7 +27,7 @@ infix 4 _∣_
 _∣_ : Rel ℤ 0ℓ
 _∣_ = ℕ._∣_ on ∣_∣
 
-pattern divides k eq  = ℕ.divides k eq
+pattern divides k eq = ℕ.divides k eq
 
 ------------------------------------------------------------------------
 -- Properties of divisibility

From 1e27632b98fdd3124d144e3588aecea890f4afa1 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sun, 3 Mar 2024 10:22:37 +0000
Subject: [PATCH 2/6] refactor to introduce new `Data.Integer.Properties`

---
 CHANGELOG.md                     | 11 ++++++++++-
 src/Data/Integer/Properties.agda | 30 +++++++++++++++++++++++-------
 2 files changed, 33 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 30b517fbc7..a9d8884777 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -127,11 +127,20 @@ Additions to existing modules
   nonZeroIndex : Fin n → ℕ.NonZero n
   ```
 
-* In `Data.Integer.Divisisbility`: introduce `divides` as an explicit pattern synonym
+* In `Data.Integer.Divisibility`: introduce `divides` as an explicit pattern synonym
   ```agda
   pattern divides k eq = Data.Nat.Divisibility.divides k eq
   ```
 
+* In `Data.Integer.Properties`:
+  ```agda
+  ◃-nonZero : {{_ : ℕ.NonZero n}} → NonZero (s ◃ n)
+  sign-*    : {{NonZero (i * j)}} → sign (i * j) ≡ sign i Sign.* sign j
+  i*j≢0     : .{{_ : NonZero i}} .{{_ : NonZero j}} → NonZero (i * j)
+  i*j≢0⇒i≢0 : .{{NonZero (i * j)}} → NonZero i
+  i*j≢0⇒j≢0 : .{{NonZero (i * j)}} → NonZero j
+  ```
+
 * In `Data.List.Relation.Unary.All.Properties`:
   ```agda
   All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs)
diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index 840b4302b5..734dc44470 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -23,7 +23,7 @@ import Data.Nat.Properties as ℕ
 open import Data.Nat.Solver
 open import Data.Product.Base using (proj₁; proj₂; _,_; _×_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
-open import Data.Sign as Sign using (Sign) renaming (_*_ to _𝕊*_)
+open import Data.Sign as Sign using (Sign)
 import Data.Sign.Properties as Sign
 open import Function.Base using (_∘_; _$_; id)
 open import Level using (0ℓ)
@@ -508,6 +508,10 @@ neg-cancel-< { -[1+ m ]} { -[1+ n ]} (+<+ m<n) = -<- (s<s⁻¹ m<n)
 ------------------------------------------------------------------------
 -- Properties of sign and _◃_
 
+◃-nonZero : ∀ s n .{{_ : ℕ.NonZero n}} → NonZero (s ◃ n)
+◃-nonZero Sign.- (ℕ.suc _) = _
+◃-nonZero Sign.+ (ℕ.suc _) = _
+
 ◃-inverse : ∀ i → sign i ◃ ∣ i ∣ ≡ i
 ◃-inverse -[1+ n ] = refl
 ◃-inverse +0       = refl
@@ -1348,7 +1352,7 @@ private
 *-assoc i j +0 rewrite
     ℕ.*-zeroʳ ∣ j ∣
   | ℕ.*-zeroʳ ∣ i ∣
-  | ℕ.*-zeroʳ ∣ sign i 𝕊* sign j ◃ ∣ i ∣ ℕ.* ∣ j ∣ ∣
+  | ℕ.*-zeroʳ ∣ sign i Sign.* sign j ◃ ∣ i ∣ ℕ.* ∣ j ∣ ∣
   = refl
 *-assoc -[1+ m ] -[1+ n ] +[1+ o ] = cong (+_ ∘ suc) (lemma m n o)
 *-assoc -[1+ m ] +[1+ n ] -[1+ o ] = cong (+_ ∘ suc) (lemma m n o)
@@ -1390,11 +1394,11 @@ private
         = refl
 *-distribʳ-+ x +0 z
   rewrite +-identityˡ z
-        | +-identityˡ (sign z 𝕊* sign x ◃ ∣ z ∣ ℕ.* ∣ x ∣)
+        | +-identityˡ (sign z Sign.* sign x ◃ ∣ z ∣ ℕ.* ∣ x ∣)
         = refl
 *-distribʳ-+ x y +0
   rewrite +-identityʳ y
-        | +-identityʳ (sign y 𝕊* sign x ◃ ∣ y ∣ ℕ.* ∣ x ∣)
+        | +-identityʳ (sign y Sign.* sign x ◃ ∣ y ∣ ℕ.* ∣ x ∣)
         = refl
 *-distribʳ-+ -[1+ m ] -[1+ n ] -[1+ o ] = cong (+_) $
   solve 3 (λ m n o → (con 2 :+ n :+ o) :* (con 1 :+ m)
@@ -1594,6 +1598,9 @@ private
 abs-* : ℤtoℕ.Homomorphic₂ ∣_∣ _*_ ℕ._*_
 abs-* i j = abs-◃ _ _
 
+sign-* : ∀ i j → {{NonZero (i * j)}} → sign (i * j) ≡ sign i Sign.* sign j
+sign-* i j rewrite abs-* i j = sign-◃ (sign i Sign.* sign j) (∣ i ∣ ℕ.* ∣ j ∣)
+
 *-cancelʳ-≡ : ∀ i j k .{{_ : NonZero k}} → i * k ≡ j * k → i ≡ j
 *-cancelʳ-≡ i j k eq with sign-cong′ eq
 ... | inj₁ s[ik]≡s[jk] = ◃-cong
@@ -1631,6 +1638,15 @@ i*j≡0⇒i≡0∨j≡0 i p with ℕ.m*n≡0⇒m≡0∨n≡0 ∣ i ∣ (abs-cong
 ... | inj₁ ∣i∣≡0 = inj₁ (∣i∣≡0⇒i≡0 ∣i∣≡0)
 ... | inj₂ ∣j∣≡0 = inj₂ (∣i∣≡0⇒i≡0 ∣j∣≡0)
 
+i*j≢0 : ∀ i j .{{_ : NonZero i}} .{{_ : NonZero j}} → NonZero (i * j)
+i*j≢0 i j rewrite abs-* i j = ℕ.m*n≢0 ∣ i ∣ ∣ j ∣
+
+i*j≢0⇒i≢0 : ∀ i {j} → .{{NonZero (i * j)}} → NonZero i
+i*j≢0⇒i≢0 i {j} rewrite abs-* i j = ℕ.m*n≢0⇒m≢0 ∣ i ∣
+
+i*j≢0⇒j≢0 : ∀ i {j} → .{{NonZero (i * j)}} → NonZero j
+i*j≢0⇒j≢0 i {j} rewrite *-comm i j = i*j≢0⇒i≢0 j {i}
+
 ------------------------------------------------------------------------
 -- Properties of _^_
 ------------------------------------------------------------------------
@@ -1704,7 +1720,7 @@ neg-distribʳ-* i j = begin
 ------------------------------------------------------------------------
 -- Properties of _*_ and _◃_
 
-◃-distrib-* :  ∀ s t m n → (s 𝕊* t) ◃ (m ℕ.* n) ≡ (s ◃ m) * (t ◃ n)
+◃-distrib-* :  ∀ s t m n → (s Sign.* t) ◃ (m ℕ.* n) ≡ (s ◃ m) * (t ◃ n)
 ◃-distrib-* s t zero    zero    = refl
 ◃-distrib-* s t zero    (suc n) = refl
 ◃-distrib-* s t (suc m) zero    =
@@ -1713,7 +1729,7 @@ neg-distribʳ-* i j = begin
     (*-comm (t ◃ zero) (s ◃ suc m))
 ◃-distrib-* s t (suc m) (suc n) =
   sym (cong₂ _◃_
-    (cong₂ _𝕊*_ (sign-◃ s (suc m)) (sign-◃ t (suc n)))
+    (cong₂ Sign._*_ (sign-◃ s (suc m)) (sign-◃ t (suc n)))
     (∣s◃m∣*∣t◃n∣≡m*n s t (suc m) (suc n)))
 
 ------------------------------------------------------------------------
@@ -1828,7 +1844,7 @@ neg-distribʳ-* i j = begin
 -- Properties of _*_ and ∣_∣
 
 ∣i*j∣≡∣i∣*∣j∣ : ∀ i j → ∣ i * j ∣ ≡ ∣ i ∣ ℕ.* ∣ j ∣
-∣i*j∣≡∣i∣*∣j∣ i j = abs-◃ (sign i 𝕊* sign j) (∣ i ∣ ℕ.* ∣ j ∣)
+∣i*j∣≡∣i∣*∣j∣ = abs-*
 
 ------------------------------------------------------------------------
 -- Properties of _⊓_ and _⊔_

From 3073aabb57271a5fcd75194d8f8ac5f59bda535c Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sun, 3 Mar 2024 10:36:17 +0000
Subject: [PATCH 3/6] refactor proofs to use new properties; streamline
 reasoning

---
 src/Data/Integer/Divisibility/Signed.agda | 50 ++++++++++-------------
 1 file changed, 22 insertions(+), 28 deletions(-)

diff --git a/src/Data/Integer/Divisibility/Signed.agda b/src/Data/Integer/Divisibility/Signed.agda
index 15fa5a4c1e..6ed4564258 100644
--- a/src/Data/Integer/Divisibility/Signed.agda
+++ b/src/Data/Integer/Divisibility/Signed.agda
@@ -29,6 +29,7 @@ import Relation.Binary.Reasoning.Preorder as ≲-Reasoning
 open import Relation.Nullary.Decidable as Dec using (yes; no)
 open import Relation.Binary.Reasoning.Syntax
 
+
 ------------------------------------------------------------------------
 -- Type
 
@@ -44,43 +45,35 @@ open _∣_ using (quotient) public
 -- Conversion between signed and unsigned divisibility
 
 ∣ᵤ⇒∣ : ∀ {k i} → k Unsigned.∣ i → k ∣ i
-∣ᵤ⇒∣ {k} {i} (Unsigned.divides 0           eq) = divides (+ 0) (∣i∣≡0⇒i≡0 eq)
+∣ᵤ⇒∣ {k} {i} (Unsigned.divides 0           eq) = divides +0 (∣i∣≡0⇒i≡0 eq)
 ∣ᵤ⇒∣ {k} {i} (Unsigned.divides q@(ℕ.suc _) eq) with k ≟ +0
 ... | yes refl = divides +0 (∣i∣≡0⇒i≡0 (trans eq (ℕ.*-zeroʳ q)))
-... | no  neq  = divides (sign i Sign.* sign k ◃ q) (◃-cong sign-eq abs-eq)
+... | no  neq  = divides s[i*k]◃q (◃-cong sign-eq abs-eq)
   where
-  ikq = sign i Sign.* sign k ◃ q
-
-  *-nonZero : ∀ m n .{{_ : ℕ.NonZero m}} .{{_ : ℕ.NonZero n}} → ℕ.NonZero (m ℕ.* n)
-  *-nonZero (ℕ.suc _) (ℕ.suc _) = _
-
-  ◃-nonZero : ∀ s n .{{_ : ℕ.NonZero n}} → NonZero (s ◃ n)
-  ◃-nonZero Sign.- (ℕ.suc _) = _
-  ◃-nonZero Sign.+ (ℕ.suc _) = _
-
-  ikq≢0 : NonZero ikq
-  ikq≢0 = ◃-nonZero (sign i Sign.* sign k) q
+  s[i*k] = sign i Sign.* sign k
+  s[i*k]◃q = s[i*k] ◃ q
 
   instance
-    ikq*∣k∣≢0 : ℕ.NonZero (∣ ikq ∣ ℕ.* ∣ k ∣)
-    ikq*∣k∣≢0 = *-nonZero ∣ ikq ∣ ∣ k ∣ {{ikq≢0}} {{≢-nonZero neq}}
+    _ = ≢-nonZero neq
+    _ = ◃-nonZero s[i*k] q
+    _ = i*j≢0 s[i*k]◃q k
 
-  sign-eq : sign i ≡ sign (ikq * k)
+  sign-eq : sign i ≡ sign (s[i*k]◃q * k)
   sign-eq = sym $ begin
-    sign (ikq * k)                        ≡⟨ sign-◃ (sign ikq Sign.* sign k) (∣ ikq ∣ ℕ.* ∣ k ∣) ⟩
-    sign ikq Sign.* sign k                ≡⟨ cong (Sign._* sign k) (sign-◃ (sign i Sign.* sign k) q) ⟩
-    (sign i Sign.* sign k) Sign.* sign k  ≡⟨ Sign.*-assoc (sign i) (sign k) (sign k) ⟩
+    sign (s[i*k]◃q * k)                   ≡⟨ sign-* s[i*k]◃q k ⟩
+    sign s[i*k]◃q Sign.* sign k           ≡⟨ cong (Sign._* _) (sign-◃ s[i*k] q) ⟩
+    s[i*k] Sign.* sign k                  ≡⟨ Sign.*-assoc (sign i) (sign k) (sign k) ⟩
     sign i Sign.* (sign k Sign.* sign k)  ≡⟨ cong (sign i Sign.*_) (Sign.s*s≡+ (sign k)) ⟩
     sign i Sign.* Sign.+                  ≡⟨ Sign.*-identityʳ (sign i) ⟩
-    sign i                          ∎
+    sign i                                ∎
     where open ≡-Reasoning
 
-  abs-eq : ∣ i ∣ ≡ ∣ ikq * k ∣
+  abs-eq : ∣ i ∣ ≡ ∣ s[i*k]◃q * k ∣
   abs-eq = sym $ begin
-    ∣ ikq * k ∣        ≡⟨ ∣i*j∣≡∣i∣*∣j∣ ikq k ⟩
-    ∣ ikq ∣ ℕ.* ∣ k ∣  ≡⟨ cong (ℕ._* ∣ k ∣) (abs-◃ (sign i Sign.* sign k) q) ⟩
-    q ℕ.* ∣ k ∣        ≡⟨ sym eq ⟩
-    ∣ i ∣              ∎
+    ∣ s[i*k]◃q * k ∣        ≡⟨ abs-* s[i*k]◃q k ⟩
+    ∣ s[i*k]◃q ∣ ℕ.* ∣ k ∣  ≡⟨ cong (ℕ._* ∣ k ∣) (abs-◃ s[i*k] q) ⟩
+    q ℕ.* ∣ k ∣             ≡⟨ eq ⟨
+    ∣ i ∣                   ∎
     where open ≡-Reasoning
 
 ∣⇒∣ᵤ : ∀ {k i} → k ∣ i → k Unsigned.∣ i
@@ -148,7 +141,7 @@ m∣∣m∣ = ∣ᵤ⇒∣ ℕ.∣-refl
 ∣m⇒∣-m : ∀ {i m} → i ∣ m → i ∣ - m
 ∣m⇒∣-m {i} {m} i∣m = ∣ᵤ⇒∣ $′ begin
   ∣ i ∣   ∣⟨ ∣⇒∣ᵤ i∣m ⟩
-  ∣ m ∣   ≡⟨ sym (∣-i∣≡∣i∣ m) ⟩
+  ∣ m ∣   ≡⟨ ∣-i∣≡∣i∣ m ⟨
   ∣ - m ∣ ∎
   where open ℕ.∣-Reasoning
 
@@ -159,7 +152,7 @@ m∣∣m∣ = ∣ᵤ⇒∣ ℕ.∣-refl
 ∣m+n∣m⇒∣n {i} {m} {n} i∣m+n i∣m = begin
   i             ∣⟨ ∣m∣n⇒∣m-n i∣m+n i∣m ⟩
   m + n - m     ≡⟨ +-comm (m + n) (- m) ⟩
-  - m + (m + n) ≡⟨ sym (+-assoc (- m) m n) ⟩
+  - m + (m + n) ≡⟨ +-assoc (- m) m n ⟨
   - m + m + n   ≡⟨ cong (_+ n) (+-inverseˡ m) ⟩
   + 0 + n       ≡⟨ +-identityˡ n ⟩
   n             ∎
@@ -171,7 +164,7 @@ m∣∣m∣ = ∣ᵤ⇒∣ ℕ.∣-refl
 ∣n⇒∣m*n : ∀ {i} m {n} → i ∣ n → i ∣ m * n
 ∣n⇒∣m*n {i} m {n} (divides q eq) = divides (m * q) $′ begin
   m * n       ≡⟨ cong (m *_) eq ⟩
-  m * (q * i) ≡⟨ sym (*-assoc m q i) ⟩
+  m * (q * i) ≡⟨ *-assoc m q i ⟨
   m * q * i   ∎
   where open ≡-Reasoning
 
@@ -189,3 +182,4 @@ m∣∣m∣ = ∣ᵤ⇒∣ ℕ.∣-refl
 
 *-cancelʳ-∣ : ∀ k {i j} .{{_ : NonZero k}} → i * k ∣ j * k → i ∣ j
 *-cancelʳ-∣ k {i} {j} = ∣ᵤ⇒∣ ∘′ Unsigned.*-cancelʳ-∣ k {i} {j} ∘′ ∣⇒∣ᵤ
+

From 5ba1a2ddaa0084521773d951d52461723fb60e26 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sun, 3 Mar 2024 10:57:39 +0000
Subject: [PATCH 4/6] remove final blank line

---
 src/Data/Integer/Divisibility/Signed.agda | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Data/Integer/Divisibility/Signed.agda b/src/Data/Integer/Divisibility/Signed.agda
index 6ed4564258..18df0c8a91 100644
--- a/src/Data/Integer/Divisibility/Signed.agda
+++ b/src/Data/Integer/Divisibility/Signed.agda
@@ -182,4 +182,3 @@ m∣∣m∣ = ∣ᵤ⇒∣ ℕ.∣-refl
 
 *-cancelʳ-∣ : ∀ k {i j} .{{_ : NonZero k}} → i * k ∣ j * k → i ∣ j
 *-cancelʳ-∣ k {i} {j} = ∣ᵤ⇒∣ ∘′ Unsigned.*-cancelʳ-∣ k {i} {j} ∘′ ∣⇒∣ᵤ
-

From f6736e23f10d1c867c82dcaeb54ad63bf715e678 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Wed, 13 Mar 2024 06:26:32 +0000
Subject: [PATCH 5/6] first review comment: missing annotation

---
 CHANGELOG.md                     | 4 ++--
 src/Data/Integer/Properties.agda | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a9d8884777..720a711b56 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -134,8 +134,8 @@ Additions to existing modules
 
 * In `Data.Integer.Properties`:
   ```agda
-  ◃-nonZero : {{_ : ℕ.NonZero n}} → NonZero (s ◃ n)
-  sign-*    : {{NonZero (i * j)}} → sign (i * j) ≡ sign i Sign.* sign j
+  ◃-nonZero : .{{_ : ℕ.NonZero n}} → NonZero (s ◃ n)
+  sign-*    : .{{NonZero (i * j)}} → sign (i * j) ≡ sign i Sign.* sign j
   i*j≢0     : .{{_ : NonZero i}} .{{_ : NonZero j}} → NonZero (i * j)
   i*j≢0⇒i≢0 : .{{NonZero (i * j)}} → NonZero i
   i*j≢0⇒j≢0 : .{{NonZero (i * j)}} → NonZero j
diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index 734dc44470..110d441b94 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -1598,7 +1598,7 @@ private
 abs-* : ℤtoℕ.Homomorphic₂ ∣_∣ _*_ ℕ._*_
 abs-* i j = abs-◃ _ _
 
-sign-* : ∀ i j → {{NonZero (i * j)}} → sign (i * j) ≡ sign i Sign.* sign j
+sign-* : ∀ i j → .{{NonZero (i * j)}} → sign (i * j) ≡ sign i Sign.* sign j
 sign-* i j rewrite abs-* i j = sign-◃ (sign i Sign.* sign j) (∣ i ∣ ℕ.* ∣ j ∣)
 
 *-cancelʳ-≡ : ∀ i j k .{{_ : NonZero k}} → i * k ≡ j * k → i ≡ j

From 3b410cff85501d9df35d71884988e5e65b92dc1e Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Wed, 13 Mar 2024 06:56:56 +0000
Subject: [PATCH 6/6] =?UTF-8?q?removed=20two=20new=20lemmas:=20`i*j?=
 =?UTF-8?q?=E2=89=A20=E2=87=92i=E2=89=A20`=20and=20`i*j=E2=89=A20=E2=87=92?=
 =?UTF-8?q?j=E2=89=A20`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                     | 2 --
 src/Data/Integer/Properties.agda | 6 ------
 2 files changed, 8 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 720a711b56..81e09a0a3a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -137,8 +137,6 @@ Additions to existing modules
   ◃-nonZero : .{{_ : ℕ.NonZero n}} → NonZero (s ◃ n)
   sign-*    : .{{NonZero (i * j)}} → sign (i * j) ≡ sign i Sign.* sign j
   i*j≢0     : .{{_ : NonZero i}} .{{_ : NonZero j}} → NonZero (i * j)
-  i*j≢0⇒i≢0 : .{{NonZero (i * j)}} → NonZero i
-  i*j≢0⇒j≢0 : .{{NonZero (i * j)}} → NonZero j
   ```
 
 * In `Data.List.Relation.Unary.All.Properties`:
diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index 110d441b94..d5706b5d53 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -1641,12 +1641,6 @@ i*j≡0⇒i≡0∨j≡0 i p with ℕ.m*n≡0⇒m≡0∨n≡0 ∣ i ∣ (abs-cong
 i*j≢0 : ∀ i j .{{_ : NonZero i}} .{{_ : NonZero j}} → NonZero (i * j)
 i*j≢0 i j rewrite abs-* i j = ℕ.m*n≢0 ∣ i ∣ ∣ j ∣
 
-i*j≢0⇒i≢0 : ∀ i {j} → .{{NonZero (i * j)}} → NonZero i
-i*j≢0⇒i≢0 i {j} rewrite abs-* i j = ℕ.m*n≢0⇒m≢0 ∣ i ∣
-
-i*j≢0⇒j≢0 : ∀ i {j} → .{{NonZero (i * j)}} → NonZero j
-i*j≢0⇒j≢0 i {j} rewrite *-comm i j = i*j≢0⇒i≢0 j {i}
-
 ------------------------------------------------------------------------
 -- Properties of _^_
 ------------------------------------------------------------------------