Skip to content

Commit 34f5009

Browse files
authored
bug: leftover from #2206 (#2564)
1 parent 0cccb39 commit 34f5009

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/Data/Nat/Properties.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ open import Algebra.Bundles using (Magma; Semigroup; CommutativeSemigroup;
1717
open import Algebra.Definitions.RawMagma using (_,_)
1818
open import Algebra.Morphism
1919
open import Algebra.Consequences.Propositional
20-
using (comm+cancelˡ⇒cancelʳ; comm∧distrʳ⇒distrˡ; comm∧distrˡ⇒distrʳ)
20+
using (commcancelˡ⇒cancelʳ; comm∧distrʳ⇒distrˡ; comm∧distrˡ⇒distrʳ)
2121
open import Algebra.Construct.NaturalChoice.Base
2222
using (MinOperator; MaxOperator)
2323
import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp
@@ -561,7 +561,7 @@ open ≤-Reasoning
561561
+-cancelˡ-≡ (suc m) _ _ eq = +-cancelˡ-≡ m _ _ (cong pred eq)
562562

563563
+-cancelʳ-≡ : RightCancellative _≡_ _+_
564-
+-cancelʳ-≡ = comm+cancelˡ⇒cancelʳ +-comm +-cancelˡ-≡
564+
+-cancelʳ-≡ = commcancelˡ⇒cancelʳ +-comm +-cancelˡ-≡
565565

566566
+-cancel-≡ : Cancellative _≡_ _+_
567567
+-cancel-≡ = +-cancelˡ-≡ , +-cancelʳ-≡

0 commit comments

Comments
 (0)