[ re agda#1752 ] add properties of ordered structures for Nat.

Author: sstucki

CHANGELOG.md

@@ -1269,6 +1269,16 @@ Other minor changes
 
   anyUpTo? : ∀ (P? : U.Decidable P) (v : ℕ) → Dec (∃ λ n → n < v × P n)
   allUpTo? : ∀ (P? : U.Decidable P) (v : ℕ) → Dec (∀ {n} → n < v → P n)
+
+  +-isPomagma               : IsPomagma _+_
+  +-isPosemigroup           : IsPosemigroup _+_
+  +-0-isPomonoid            : IsPomonoid _+_ 0
+  +-0-isCommutativePomonoid : IsCommutativePomonoid _+_ 0
+  +-0-commutativePomonoid   : CommutativePomonoid 0ℓ 0ℓ 0ℓ
+  +-*-isPosemiring          : IsPosemiring _+_ _*_ 0 1
+  *-1-isCommutativePomonoid : IsCommutativePomonoid _*_ 1
+  +-*-posemiring            : Posemiring 0ℓ 0ℓ 0ℓ
+  *-1-commutativePomonoid   : CommutativePomonoid 0ℓ 0ℓ 0ℓ
   ```
 
 * Added new functions in `Data.Nat`:

src/Data/Nat/Properties.agda

@@ -13,6 +13,7 @@ module Data.Nat.Properties where
 
 open import Axiom.UniquenessOfIdentityProofs
 open import Algebra.Bundles
+open import Algebra.Ordered.Bundles
 open import Algebra.Morphism
 open import Algebra.Consequences.Propositional
 open import Algebra.Construct.NaturalChoice.Base
@@ -44,6 +45,7 @@ open import Algebra.Definitions {A = ℕ} _≡_
 open import Algebra.Definitions
   using (LeftCancellative; RightCancellative; Cancellative)
 open import Algebra.Structures {A = ℕ} _≡_
+import Algebra.Ordered.Structures as OrderedStructures
 
 ------------------------------------------------------------------------
 -- Properties of NonZero
@@ -537,111 +539,6 @@ open ≤-Reasoning
 +-cancel-≡ : Cancellative _≡_ _+_
 +-cancel-≡ = +-cancelˡ-≡ , +-cancelʳ-≡
 
-------------------------------------------------------------------------
--- Structures
-
-+-isMagma : IsMagma _+_
-+-isMagma = record
-  { isEquivalence = isEquivalence
-  ; ∙-cong        = cong₂ _+_
-  }
-
-+-isSemigroup : IsSemigroup _+_
-+-isSemigroup = record
-  { isMagma = +-isMagma
-  ; assoc   = +-assoc
-  }
-
-+-isCommutativeSemigroup : IsCommutativeSemigroup _+_
-+-isCommutativeSemigroup = record
-  { isSemigroup = +-isSemigroup
-  ; comm        = +-comm
-  }
-
-+-0-isMonoid : IsMonoid _+_ 0
-+-0-isMonoid = record
-  { isSemigroup = +-isSemigroup
-  ; identity    = +-identity
-  }
-
-+-0-isCommutativeMonoid : IsCommutativeMonoid _+_ 0
-+-0-isCommutativeMonoid = record
-  { isMonoid = +-0-isMonoid
-  ; comm     = +-comm
-  }
-
-------------------------------------------------------------------------
--- Raw bundles
-
-+-rawMagma : RawMagma 0ℓ 0ℓ
-+-rawMagma = record
-  { _≈_ = _≡_
-  ; _∙_ = _+_
-  }
-
-+-0-rawMonoid : RawMonoid 0ℓ 0ℓ
-+-0-rawMonoid = record
-  { _≈_ = _≡_
-  ; _∙_ = _+_
-  ; ε   = 0
-  }
-
-------------------------------------------------------------------------
--- Bundles
-
-+-magma : Magma 0ℓ 0ℓ
-+-magma = record
-  { isMagma = +-isMagma
-  }
-
-+-semigroup : Semigroup 0ℓ 0ℓ
-+-semigroup = record
-  { isSemigroup = +-isSemigroup
-  }
-
-+-commutativeSemigroup : CommutativeSemigroup 0ℓ 0ℓ
-+-commutativeSemigroup = record
-  { isCommutativeSemigroup = +-isCommutativeSemigroup
-  }
-
-+-0-monoid : Monoid 0ℓ 0ℓ
-+-0-monoid = record
-  { isMonoid = +-0-isMonoid
-  }
-
-+-0-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
-+-0-commutativeMonoid = record
-  { isCommutativeMonoid = +-0-isCommutativeMonoid
-  }
-
-∸-magma : Magma 0ℓ 0ℓ
-∸-magma = magma _∸_
-
-
-------------------------------------------------------------------------
--- Other properties of _+_ and _≡_
-
-m≢1+m+n : ∀ m {n} → m ≢ suc (m + n)
-m≢1+m+n (suc m) eq = m≢1+m+n m (cong pred eq)
-
-m≢1+n+m : ∀ m {n} → m ≢ suc (n + m)
-m≢1+n+m m m≡1+n+m = m≢1+m+n m (trans m≡1+n+m (cong suc (+-comm _ m)))
-
-m+1+n≢m : ∀ m {n} → m + suc n ≢ m
-m+1+n≢m (suc m) = (m+1+n≢m m) ∘ suc-injective
-
-m+1+n≢n : ∀ m {n} → m + suc n ≢ n
-m+1+n≢n m {n} rewrite +-suc m n = ≢-sym (m≢1+n+m n)
-
-m+1+n≢0 : ∀ m {n} → m + suc n ≢ 0
-m+1+n≢0 m {n} rewrite +-suc m n = λ()
-
-m+n≡0⇒m≡0 : ∀ m {n} → m + n ≡ 0 → m ≡ 0
-m+n≡0⇒m≡0 zero eq = refl
-
-m+n≡0⇒n≡0 : ∀ m {n} → m + n ≡ 0 → n ≡ 0
-m+n≡0⇒n≡0 m {n} m+n≡0 = m+n≡0⇒m≡0 n (trans (+-comm n m) (m+n≡0))
-
 ------------------------------------------------------------------------
 -- Properties of _+_ and _≤_/_<_
 
@@ -732,6 +629,107 @@ m+n≮n (suc m) (suc n) (s<s m+n<n) = m+n≮n m (suc n) (<-step m+n<n)
 m+n≮m : ∀ m n → m + n ≮ m
 m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m)
 
+------------------------------------------------------------------------
+-- Structures
+
+open OrderedStructures _≡_ _≤_
+
++-isPomagma : IsPomagma _+_
++-isPomagma = record
+  { isPartialOrder = ≤-isPartialOrder
+  ; mono           = +-mono-≤
+  }
+
++-isPosemigroup : IsPosemigroup _+_
++-isPosemigroup = record
+  { isPomagma = +-isPomagma
+  ; assoc     = +-assoc
+  }
+
++-0-isPomonoid : IsPomonoid _+_ 0
++-0-isPomonoid = record
+  { isPosemigroup = +-isPosemigroup
+  ; identity      = +-identity
+  }
+
++-0-isCommutativePomonoid : IsCommutativePomonoid _+_ 0
++-0-isCommutativePomonoid = record
+  { isPomonoid = +-0-isPomonoid
+  ; comm       = +-comm
+  }
+
+open IsCommutativePomonoid +-0-isCommutativePomonoid public using ()
+  renaming
+  ( isMagma                to +-isMagma
+  ; isSemigroup            to +-isSemigroup
+  ; isCommutativeSemigroup to +-isCommutativeSemigroup
+  ; isMonoid               to +-0-isMonoid
+  ; isCommutativeMonoid    to +-0-isCommutativeMonoid
+  )
+
+------------------------------------------------------------------------
+-- Raw bundles
+
++-rawMagma : RawMagma 0ℓ 0ℓ
++-rawMagma = record
+  { _≈_ = _≡_
+  ; _∙_ = _+_
+  }
+
++-0-rawMonoid : RawMonoid 0ℓ 0ℓ
++-0-rawMonoid = record
+  { _≈_ = _≡_
+  ; _∙_ = _+_
+  ; ε   = 0
+  }
+
+------------------------------------------------------------------------
+-- Bundles
+
++-0-commutativePomonoid : CommutativePomonoid 0ℓ 0ℓ 0ℓ
++-0-commutativePomonoid = record
+  { isCommutativePomonoid = +-0-isCommutativePomonoid
+  }
+
+open CommutativePomonoid +-0-commutativePomonoid public using () renaming
+  ( magma                to +-magma
+  ; pomagma              to +-pomagma
+  ; semigroup            to +-semigroup
+  ; posemigroup          to +-posemigroup
+  ; commutativeSemigroup to +-commutativeSemigroup
+  ; monoid               to +-0-monoid
+  ; pomonoid             to +-0-pomonoid
+  ; commutativeMonoid    to +-0-commutativeMonoid
+  )
+
+∸-magma : Magma 0ℓ 0ℓ
+∸-magma = magma _∸_
+
+------------------------------------------------------------------------
+-- Other properties of _+_ and _≡_
+
+m≢1+m+n : ∀ m {n} → m ≢ suc (m + n)
+m≢1+m+n (suc m) eq = m≢1+m+n m (cong pred eq)
+
+m≢1+n+m : ∀ m {n} → m ≢ suc (n + m)
+m≢1+n+m m m≡1+n+m = m≢1+m+n m (trans m≡1+n+m (cong suc (+-comm _ m)))
+
+m+1+n≢m : ∀ m {n} → m + suc n ≢ m
+m+1+n≢m (suc m) = (m+1+n≢m m) ∘ suc-injective
+
+m+1+n≢n : ∀ m {n} → m + suc n ≢ n
+m+1+n≢n m {n} rewrite +-suc m n = ≢-sym (m≢1+n+m n)
+
+m+1+n≢0 : ∀ m {n} → m + suc n ≢ 0
+m+1+n≢0 m {n} rewrite +-suc m n = λ()
+
+m+n≡0⇒m≡0 : ∀ m {n} → m + n ≡ 0 → m ≡ 0
+m+n≡0⇒m≡0 zero eq = refl
+
+m+n≡0⇒n≡0 : ∀ m {n} → m + n ≡ 0 → n ≡ 0
+m+n≡0⇒n≡0 m {n} m+n≡0 = m+n≡0⇒m≡0 n (trans (+-comm n m) (m+n≡0))
+
+
 ------------------------------------------------------------------------
 -- Properties of _*_
 ------------------------------------------------------------------------
@@ -804,48 +802,101 @@ m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m)
   suc m * (n * o)     ∎
 
 ------------------------------------------------------------------------
--- Structures
+-- Other properties of _*_ and _≤_/_<_
 
-*-isMagma : IsMagma _*_
-*-isMagma = record
-  { isEquivalence = isEquivalence
-  ; ∙-cong        = cong₂ _*_
-  }
+*-cancelʳ-≤ : ∀ m n o .{{_ : NonZero o}} → m * o ≤ n * o → m ≤ n
+*-cancelʳ-≤ zero    _       (suc o) _  = z≤n
+*-cancelʳ-≤ (suc m) (suc n) (suc o) le =
+  s≤s (*-cancelʳ-≤ m n (suc o) (+-cancelˡ-≤ (suc o) le))
 
-*-isSemigroup : IsSemigroup _*_
-*-isSemigroup = record
-  { isMagma = *-isMagma
-  ; assoc   = *-assoc
-  }
+*-cancelˡ-≤ : ∀ {m n} o .{{_ : NonZero o}} → o * m ≤ o * n → m ≤ n
+*-cancelˡ-≤ {m} {n} o rewrite *-comm o m | *-comm o n = *-cancelʳ-≤ m n o
 
-*-isCommutativeSemigroup : IsCommutativeSemigroup _*_
-*-isCommutativeSemigroup = record
-  { isSemigroup = *-isSemigroup
-  ; comm        = *-comm
-  }
+*-mono-≤ : _*_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
+*-mono-≤ z≤n       _   = z≤n
+*-mono-≤ (s≤s m≤n) u≤v = +-mono-≤ u≤v (*-mono-≤ m≤n u≤v)
 
-*-1-isMonoid : IsMonoid _*_ 1
-*-1-isMonoid = record
-  { isSemigroup = *-isSemigroup
-  ; identity    = *-identity
-  }
+*-monoˡ-≤ : ∀ n → (_* n) Preserves _≤_ ⟶ _≤_
+*-monoˡ-≤ n m≤o = *-mono-≤ m≤o (≤-refl {n})
 
-*-1-isCommutativeMonoid : IsCommutativeMonoid _*_ 1
-*-1-isCommutativeMonoid = record
-  { isMonoid = *-1-isMonoid
-  ; comm     = *-comm
+*-monoʳ-≤ : ∀ n → (n *_) Preserves _≤_ ⟶ _≤_
+*-monoʳ-≤ n m≤o = *-mono-≤ (≤-refl {n}) m≤o
+
+*-mono-< : _*_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
+*-mono-< z<s               u<v@(s≤s _) = 0<1+n
+*-mono-< (s<s m<n@(s≤s _)) u<v@(s≤s _) = +-mono-< u<v (*-mono-< m<n u<v)
+
+*-monoˡ-< : ∀ n .{{_ : NonZero n}} → (_* n) Preserves _<_ ⟶ _<_
+*-monoˡ-< (suc n) z<s       = 0<1+n
+*-monoˡ-< (suc n) (s<s m<o@(s≤s _)) =
+  +-mono-≤-< (≤-refl {suc n}) (*-monoˡ-< (suc n) m<o)
+
+*-monoʳ-< : ∀ n .{{_ : NonZero n}} → (n *_) Preserves _<_ ⟶ _<_
+*-monoʳ-< (suc zero)    m<o@(s≤s _) = +-mono-≤ m<o z≤n
+*-monoʳ-< (suc (suc n)) m<o@(s≤s _) =
+  +-mono-≤ m<o (<⇒≤ (*-monoʳ-< (suc n) m<o))
+
+m≤m*n : ∀ m n .{{_ : NonZero n}} → m ≤ m * n
+m≤m*n m n@(suc _) = begin
+  m     ≡⟨ sym (*-identityʳ m) ⟩
+  m * 1 ≤⟨ *-monoʳ-≤ m 0<1+n ⟩
+  m * n ∎
+
+m≤n*m : ∀ m n .{{_ : NonZero n}} → m ≤ n * m
+m≤n*m m n@(suc _) = begin
+  m     ≤⟨ m≤m*n m n ⟩
+  m * n ≡⟨ *-comm m n ⟩
+  n * m ∎
+
+m<m*n : ∀ m n .{{_ : NonZero m}} → 1 < n → m < m * n
+m<m*n m@(suc m-1) n@(suc (suc n-2)) (s≤s (s≤s _)) = begin-strict
+  m           <⟨ s≤s (s≤s (m≤n+m m-1 n-2)) ⟩
+  n + m-1     ≤⟨ +-monoʳ-≤ n (m≤m*n m-1 n) ⟩
+  n + m-1 * n ≡⟨⟩
+  m * n       ∎
+
+*-cancelʳ-< : RightCancellative _<_ _*_
+*-cancelʳ-< {zero}  zero    (suc o) _     = 0<1+n
+*-cancelʳ-< {suc m} zero    (suc o) _     = 0<1+n
+*-cancelʳ-< {m}     (suc n) (suc o) nm<om =
+  s≤s (*-cancelʳ-< n o (+-cancelˡ-< m nm<om))
+
+*-cancelˡ-< : LeftCancellative _<_ _*_
+*-cancelˡ-< x {y} {z} rewrite *-comm x y | *-comm x z = *-cancelʳ-< y z
+
+*-cancel-< : Cancellative _<_ _*_
+*-cancel-< = *-cancelˡ-< , *-cancelʳ-<
+
+------------------------------------------------------------------------
+-- Structures
+
++-*-isPosemiring : IsPosemiring _+_ _*_ 0 1
++-*-isPosemiring = record
+  { +-isCommutativePomonoid = +-0-isCommutativePomonoid
+  ; *-mono                  = *-mono-≤
+  ; *-assoc                 = *-assoc
+  ; *-identity              = *-identity
+  ; distrib                 = *-distrib-+
+  ; zero                    = *-zero
   }
 
-+-*-isSemiring : IsSemiring _+_ _*_ 0 1
-+-*-isSemiring = record
-  { isSemiringWithoutAnnihilatingZero = record
-    { +-isCommutativeMonoid = +-0-isCommutativeMonoid
-    ; *-cong                = cong₂ _*_
-    ; *-assoc               = *-assoc
-    ; *-identity            = *-identity
-    ; distrib               = *-distrib-+
-    }
-  ; zero = *-zero
+open IsPosemiring +-*-isPosemiring public
+  using
+  ( *-isMagma
+  ; *-isSemigroup
+  ; *-isPomagma
+  ; *-isPosemigroup
+  )
+  renaming
+  ( *-isMonoid              to *-1-isMonoid
+  ; *-isPomonoid            to *-1-isPomonoid
+  ; isSemiring              to +-*-isSemiring
+  )
+
+*-1-isCommutativePomonoid : IsCommutativePomonoid _*_ 1
+*-1-isCommutativePomonoid = record
+  { isPomonoid = *-1-isPomonoid
+  ; comm       = *-comm
   }
 
 +-*-isCommutativeSemiring : IsCommutativeSemiring _+_ _*_ 0 1
@@ -855,7 +906,7 @@ m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m)
   }
 
 ------------------------------------------------------------------------
--- Bundles
+-- Raw bundles
 
 *-rawMagma : RawMagma 0ℓ 0ℓ
 *-rawMagma = record
@@ -870,35 +921,40 @@ m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m)
   ; ε   = 1
   }
 
-*-magma : Magma 0ℓ 0ℓ
-*-magma = record
-  { isMagma = *-isMagma
-  }
-
-*-semigroup : Semigroup 0ℓ 0ℓ
-*-semigroup = record
-  { isSemigroup = *-isSemigroup
-  }
+------------------------------------------------------------------------
+-- Bundles
 
-*-commutativeSemigroup : CommutativeSemigroup 0ℓ 0ℓ
-*-commutativeSemigroup = record
-  { isCommutativeSemigroup = *-isCommutativeSemigroup
++-*-posemiring : Posemiring 0ℓ 0ℓ 0ℓ
++-*-posemiring = record
+  { isPosemiring = +-*-isPosemiring
   }
 
-*-1-monoid : Monoid 0ℓ 0ℓ
-*-1-monoid = record
-  { isMonoid = *-1-isMonoid
-  }
+open Posemiring +-*-posemiring public
+  using
+  ( *-magma
+  ; *-pomagma
+  ; *-semigroup
+  ; *-posemigroup
+  ; *-isPomagma
+  ; *-isPosemigroup
+  )
+  renaming
+  ( *-monoid                to *-1-monoid
+  ; *-pomonoid              to *-1-pomonoid
+  ; semiring                to +-*-semiring
+  )
 
-*-1-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
-*-1-commutativeMonoid = record
-  { isCommutativeMonoid = *-1-isCommutativeMonoid
+*-1-commutativePomonoid : CommutativePomonoid 0ℓ 0ℓ 0ℓ
+*-1-commutativePomonoid = record
+  { isCommutativePomonoid = *-1-isCommutativePomonoid
   }
 
-+-*-semiring : Semiring 0ℓ 0ℓ
-+-*-semiring = record
-  { isSemiring = +-*-isSemiring
-  }
+open CommutativePomonoid *-1-commutativePomonoid public using () renaming
+  ( isCommutativeSemigroup to *-isCommutativeSemigroup
+  ; commutativeSemigroup   to *-commutativeSemigroup
+  ; isCommutativeMonoid    to *-1-isCommutativeMonoid
+  ; commutativeMonoid      to *-1-commutativeMonoid
+  )
 
 +-*-commutativeSemiring : CommutativeSemiring 0ℓ 0ℓ
 +-*-commutativeSemiring = record
@@ -943,72 +999,6 @@ m*n≡1⇒n≡1 m n eq = m*n≡1⇒m≡1 n m (trans (*-comm n m) eq)
   (m * o) * (n * p) ∎
   where open CommSemigroupProperties *-commutativeSemigroup
 
-------------------------------------------------------------------------
--- Other properties of _*_ and _≤_/_<_
-
-*-cancelʳ-≤ : ∀ m n o .{{_ : NonZero o}} → m * o ≤ n * o → m ≤ n
-*-cancelʳ-≤ zero    _       (suc o) _  = z≤n
-*-cancelʳ-≤ (suc m) (suc n) (suc o) le =
-  s≤s (*-cancelʳ-≤ m n (suc o) (+-cancelˡ-≤ (suc o) le))
-
-*-cancelˡ-≤ : ∀ {m n} o .{{_ : NonZero o}} → o * m ≤ o * n → m ≤ n
-*-cancelˡ-≤ {m} {n} o rewrite *-comm o m | *-comm o n = *-cancelʳ-≤ m n o
-
-*-mono-≤ : _*_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
-*-mono-≤ z≤n       _   = z≤n
-*-mono-≤ (s≤s m≤n) u≤v = +-mono-≤ u≤v (*-mono-≤ m≤n u≤v)
-
-*-monoˡ-≤ : ∀ n → (_* n) Preserves _≤_ ⟶ _≤_
-*-monoˡ-≤ n m≤o = *-mono-≤ m≤o (≤-refl {n})
-
-*-monoʳ-≤ : ∀ n → (n *_) Preserves _≤_ ⟶ _≤_
-*-monoʳ-≤ n m≤o = *-mono-≤ (≤-refl {n}) m≤o
-
-*-mono-< : _*_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
-*-mono-< z<s               u<v@(s≤s _) = 0<1+n
-*-mono-< (s<s m<n@(s≤s _)) u<v@(s≤s _) = +-mono-< u<v (*-mono-< m<n u<v)
-
-*-monoˡ-< : ∀ n .{{_ : NonZero n}} → (_* n) Preserves _<_ ⟶ _<_
-*-monoˡ-< (suc n) z<s       = 0<1+n
-*-monoˡ-< (suc n) (s<s m<o@(s≤s _)) =
-  +-mono-≤-< (≤-refl {suc n}) (*-monoˡ-< (suc n) m<o)
-
-*-monoʳ-< : ∀ n .{{_ : NonZero n}} → (n *_) Preserves _<_ ⟶ _<_
-*-monoʳ-< (suc zero)    m<o@(s≤s _) = +-mono-≤ m<o z≤n
-*-monoʳ-< (suc (suc n)) m<o@(s≤s _) =
-  +-mono-≤ m<o (<⇒≤ (*-monoʳ-< (suc n) m<o))
-
-m≤m*n : ∀ m n .{{_ : NonZero n}} → m ≤ m * n
-m≤m*n m n@(suc _) = begin
-  m     ≡⟨ sym (*-identityʳ m) ⟩
-  m * 1 ≤⟨ *-monoʳ-≤ m 0<1+n ⟩
-  m * n ∎
-
-m≤n*m : ∀ m n .{{_ : NonZero n}} → m ≤ n * m
-m≤n*m m n@(suc _) = begin
-  m     ≤⟨ m≤m*n m n ⟩
-  m * n ≡⟨ *-comm m n ⟩
-  n * m ∎
-
-m<m*n : ∀ m n .{{_ : NonZero m}} → 1 < n → m < m * n
-m<m*n m@(suc m-1) n@(suc (suc n-2)) (s≤s (s≤s _)) = begin-strict
-  m           <⟨ s≤s (s≤s (m≤n+m m-1 n-2)) ⟩
-  n + m-1     ≤⟨ +-monoʳ-≤ n (m≤m*n m-1 n) ⟩
-  n + m-1 * n ≡⟨⟩
-  m * n       ∎
-
-*-cancelʳ-< : RightCancellative _<_ _*_
-*-cancelʳ-< {zero}  zero    (suc o) _     = 0<1+n
-*-cancelʳ-< {suc m} zero    (suc o) _     = 0<1+n
-*-cancelʳ-< {m}     (suc n) (suc o) nm<om =
-  s≤s (*-cancelʳ-< n o (+-cancelˡ-< m nm<om))
-
-*-cancelˡ-< : LeftCancellative _<_ _*_
-*-cancelˡ-< x {y} {z} rewrite *-comm x y | *-comm x z = *-cancelʳ-< y z
-
-*-cancel-< : Cancellative _<_ _*_
-*-cancel-< = *-cancelˡ-< , *-cancelʳ-<
-
 ------------------------------------------------------------------------
 -- Properties of _^_
 ------------------------------------------------------------------------