[ refactor ] Revise definitions, consequences, and use, of Algebra.Definitions.(Almost)*Cancellative

doc/README.agda

@@ -3,7 +3,7 @@
 module README where
 
 ------------------------------------------------------------------------
--- The Agda standard library, version 2.3-dev
+-- The Agda standard library, version 3.0-dev
 --
 -- Authors: Nils Anders Danielsson, Matthew Daggitt, Guillaume Allais
 -- with contributions from Andreas Abel, Stevan Andjelkovic,

src/Algebra/Consequences/Base.agda

@@ -13,14 +13,48 @@ module Algebra.Consequences.Base
 open import Algebra.Core
 open import Algebra.Definitions
 open import Data.Sum.Base
+open import Function.Base using (const)
 open import Relation.Binary.Core
 open import Relation.Binary.Definitions using (Reflexive)
+open import Relation.Nullary.Decidable.Core using (yes; no)
+open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Unary using (Pred; Decidable)
+
 
 module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where
 
   sel⇒idem : Selective _≈_ _•_ → Idempotent _≈_ _•_
   sel⇒idem sel x = reduce (sel x x)
 
+module _ {p ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) (P : Pred A p) where
+
+  almost⇒exceptˡ : _-AlmostLeftCancellative_ _≈_ P _•_ →
+                   Except_-LeftCancellative_ _≈_ P _•_
+  almost⇒exceptˡ cancelˡ {x} with cancelˡ x
+  ... | inj₁ px     = contradiction px
+  ... | inj₂ cancel = const cancel
+
+  almost⇒exceptʳ : _-AlmostRightCancellative_ _≈_ P _•_ →
+                   Except_-RightCancellative_ _≈_ P _•_
+  almost⇒exceptʳ cancelʳ {x} with cancelʳ x
+  ... | inj₁ px     = contradiction px
+  ... | inj₂ cancel = const cancel
+
+module _ {p ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ)
+         {P : Pred A p} (dec : Decidable P) where
+
+  except⇒almostˡ : Except_-LeftCancellative_ _≈_ P _•_ →
+                   _-AlmostLeftCancellative_ _≈_ P _•_
+  except⇒almostˡ cancelˡ x with dec x
+  ... | yes px = inj₁ px
+  ... | no ¬px = inj₂ (cancelˡ ¬px)
+
+  except⇒almostʳ : Except_-RightCancellative_ _≈_ P _•_ →
+                   _-AlmostRightCancellative_ _≈_ P _•_
+  except⇒almostʳ cancelʳ x with dec x
+  ... | yes px = inj₁ px
+  ... | no ¬px = inj₂ (cancelʳ ¬px)
+
 module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where
 
   reflexive∧selfInverse⇒involutive : Reflexive _≈_ →

src/Algebra/Consequences/Setoid.agda

@@ -157,17 +157,19 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where
 
   comm∧almostCancelˡ⇒almostCancelʳ : AlmostLeftCancellative e _∙_ →
                                      AlmostRightCancellative e _∙_
-  comm∧almostCancelˡ⇒almostCancelʳ cancelˡ-nonZero x y z x≉e yx≈zx =
-    cancelˡ-nonZero x y z x≉e $ begin
+  comm∧almostCancelˡ⇒almostCancelʳ almostCancelˡ x with almostCancelˡ x
+  ... | inj₁ x≈e     = inj₁ x≈e
+  ... | inj₂ cancelˡ = inj₂ λ y z yx≈zx → cancelˡ y z $ begin
       x ∙ y ≈⟨ comm x y ⟩
       y ∙ x ≈⟨ yx≈zx ⟩
       z ∙ x ≈⟨ comm z x ⟩
       x ∙ z ∎
 
   comm∧almostCancelʳ⇒almostCancelˡ : AlmostRightCancellative e _∙_ →
                                      AlmostLeftCancellative e _∙_
-  comm∧almostCancelʳ⇒almostCancelˡ cancelʳ-nonZero x y z x≉e xy≈xz =
-    cancelʳ-nonZero x y z x≉e $ begin
+  comm∧almostCancelʳ⇒almostCancelˡ almostCancelʳ x with almostCancelʳ x
+  ... | inj₁ x≈e     = inj₁ x≈e
+  ... | inj₂ cancelʳ = inj₂ λ y z xy≈xz → cancelʳ y z $ begin
       y ∙ x ≈⟨ comm y x ⟩
       x ∙ y ≈⟨ xy≈xz ⟩
       x ∙ z ≈⟨ comm x z ⟩

src/Algebra/Definitions.agda

@@ -16,7 +16,6 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
-open import Relation.Nullary.Negation.Core using (¬_)
 
 module Algebra.Definitions
   {a ℓ} {A : Set a}   -- The underlying set
@@ -26,6 +25,8 @@ module Algebra.Definitions
 open import Algebra.Core using (Op₁; Op₂)
 open import Data.Product.Base using (_×_; ∃-syntax)
 open import Data.Sum.Base using (_⊎_)
+open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Unary using (Pred)
 
 ------------------------------------------------------------------------
 -- Properties of operations
@@ -37,10 +38,10 @@ Congruent₂ : Op₂ A → Set _
 Congruent₂ ∙ = ∙ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
 
 LeftCongruent : Op₂ A → Set _
-LeftCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _≈_ ⟶ _≈_
+LeftCongruent _∙_ = ∀ {x} → Congruent₁ (x ∙_)
 
 RightCongruent : Op₂ A → Set _
-RightCongruent _∙_ = ∀ {x} → (_∙ x) Preserves _≈_ ⟶ _≈_
+RightCongruent _∙_ = ∀ {x} → Congruent₁ (_∙ x)
 
 Associative : Op₂ A → Set _
 Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z))
@@ -140,20 +141,36 @@ SelfInverse f = ∀ {x y} → f x ≈ y → f y ≈ x
 Involutive : Op₁ A → Set _
 Involutive f = ∀ x → f (f x) ≈ x
 
+LeftCancellativeAt : A → Op₂ A → Set _
+LeftCancellativeAt x _•_ = ∀ y z → (x • y) ≈ (x • z) → y ≈ z
+
 LeftCancellative : Op₂ A → Set _
-LeftCancellative _•_ = ∀ x y z → (x • y) ≈ (x • z) → y ≈ z
+LeftCancellative _•_ = ∀ x → LeftCancellativeAt x _•_
+
+RightCancellativeAt : A → Op₂ A → Set _
+RightCancellativeAt x _•_ = ∀ y z → (y • x) ≈ (z • x) → y ≈ z
 
 RightCancellative : Op₂ A → Set _
-RightCancellative _•_ = ∀ x y z → (y • x) ≈ (z • x) → y ≈ z
+RightCancellative _•_ = ∀ x → RightCancellativeAt x _•_
 
 Cancellative : Op₂ A → Set _
 Cancellative _•_ = (LeftCancellative _•_) × (RightCancellative _•_)
 
+_-AlmostLeftCancellative_ Except_-LeftCancellative_ : ∀ {p} (P : Pred A p) →
+                                                      Op₂ A → Set _
+P -AlmostLeftCancellative _•_ = ∀ x → P x ⊎ LeftCancellativeAt x _•_
+Except P -LeftCancellative _•_ = ∀ {x} → ¬ (P x) → LeftCancellativeAt x _•_
+
 AlmostLeftCancellative : A → Op₂ A → Set _
-AlmostLeftCancellative e _•_ = ∀ x y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z
+AlmostLeftCancellative e = (_≈ e) -AlmostLeftCancellative_
+
+_-AlmostRightCancellative_ Except_-RightCancellative_ : ∀ {p} (P : Pred A p) →
+                                                         Op₂ A → Set _
+P -AlmostRightCancellative _•_ = ∀ x → P x ⊎ RightCancellativeAt x _•_
+Except P -RightCancellative _•_ = ∀ {x} → ¬ (P x) → RightCancellativeAt x _•_
 
 AlmostRightCancellative : A → Op₂ A → Set _
-AlmostRightCancellative e _•_ = ∀ x y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z
+AlmostRightCancellative e = (_≈ e) -AlmostRightCancellative_
 
 AlmostCancellative : A → Op₂ A → Set _
 AlmostCancellative e _•_ = AlmostLeftCancellative e _•_ × AlmostRightCancellative e _•_

src/Algebra/Properties/CancellativeCommutativeSemiring.agda

@@ -25,13 +25,9 @@ open import Relation.Binary.Reasoning.Setoid setoid
 *-almostCancelʳ = comm+almostCancelˡ⇒almostCancelʳ *-comm *-cancelˡ-nonZero
 
 xy≈0⇒x≈0∨y≈0 : Decidable _≈_ → ∀ {x y} → x * y ≈ 0# → x ≈ 0# ⊎ y ≈ 0#
-xy≈0⇒x≈0∨y≈0 _≟_ {x} {y} xy≈0 with x ≟ 0# | y ≟ 0#
-... | yes x≈0 | _       = inj₁ x≈0
-... | no  _   | yes y≈0 = inj₂ y≈0
-... | no  x≉0 | no  y≉0 = contradiction y≈0 y≉0
-  where
-  xy≈x*0 = trans xy≈0 (sym (zeroʳ x))
-  y≈0    = *-cancelˡ-nonZero _ y 0# x≉0 xy≈x*0
+xy≈0⇒x≈0∨y≈0 _≟_ {x} {y} xy≈0 with *-cancelˡ-nonZero x
+... | inj₁ x≈0     = inj₁ x≈0
+... | inj₂ cancelˡ = inj₂ (cancelˡ y 0# (trans xy≈0 (sym (zeroʳ x))))
 
 x≉0∧y≉0⇒xy≉0 : Decidable _≈_ → ∀ {x y} → x ≉ 0# → y ≉ 0# → x * y ≉ 0#
 x≉0∧y≉0⇒xy≉0 _≟_ x≉0 y≉0 xy≈0 with xy≈0⇒x≈0∨y≈0 _≟_ xy≈0

src/Algebra/Properties/Semiring/Primality.agda

@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Some theory for CancellativeCommutativeSemiring.
+-- Properties of Coprimality and Irreducibility for Semiring.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
@@ -15,8 +15,11 @@ module Algebra.Properties.Semiring.Primality
   {a ℓ} (R : Semiring a ℓ)
   where
 
-open Semiring R renaming (Carrier to A)
+open Semiring R
+  using (_≉_; sym; trans; 0#; 1#; zeroˡ; rawSemiring)
+  renaming (Carrier to A)
 open import Algebra.Properties.Semiring.Divisibility R
+  using (_∣_; ∣-trans; 0∤1)
 
 ------------------------------------------------------------------------
 -- Re-export primality definitions

src/Data/Integer/Properties.agda

@@ -44,7 +44,7 @@ open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 import Relation.Nullary.Decidable as Dec
 
 open import Algebra.Definitions {A = ℤ} _≡_
-open import Algebra.Consequences.Propositional
+open import Algebra.Consequences.Propositional {A = ℤ}
 open import Algebra.Structures {A = ℤ} _≡_
 module ℤtoℕ = Morphism.Definitions ℤ ℕ _≡_
 module ℕtoℤ = Morphism.Definitions ℕ ℤ _≡_

src/Data/Nat/Properties.agda

@@ -16,8 +16,6 @@ open import Algebra.Bundles using (Magma; Semigroup; CommutativeSemigroup;
   CommutativeMonoid; Monoid; Semiring; CommutativeSemiring; CommutativeSemiringWithoutOne)
 open import Algebra.Definitions.RawMagma using (_,_)
 open import Algebra.Morphism
-open import Algebra.Consequences.Propositional
-  using (comm∧cancelˡ⇒cancelʳ; comm∧distrʳ⇒distrˡ; comm∧distrˡ⇒distrʳ)
 open import Algebra.Construct.NaturalChoice.Base
   using (MinOperator; MaxOperator)
 import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp
@@ -46,6 +44,10 @@ open import Relation.Nullary.Decidable using (True; via-injection; map′; recom
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Reflects using (fromEquivalence)
 
+open import Algebra.Consequences.Propositional {A = ℕ}
+  using ( comm∧cancelˡ⇒cancelʳ
+        ; comm∧distrʳ⇒distrˡ; comm∧distrˡ⇒distrʳ
+        ; almost⇒exceptʳ)
 open import Algebra.Definitions {A = ℕ} _≡_
   hiding (LeftCancellative; RightCancellative; Cancellative)
 open import Algebra.Definitions
@@ -908,10 +910,16 @@ m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m)
 ------------------------------------------------------------------------
 -- Other properties of _*_ and _≡_
 
+*-almostCancelʳ-≡ : AlmostRightCancellative 0 _*_
+*-almostCancelʳ-≡ zero    = inj₁ refl
+*-almostCancelʳ-≡ o@(suc _) = inj₂ lemma
+  module *-AlmostRightCancellative where
+  lemma : RightCancellativeAt o _*_
+  lemma zero    zero    _  = refl
+  lemma (suc m) (suc n) eq = cong suc (lemma m n (+-cancelˡ-≡ o (m * o) (n * o) eq))
+
 *-cancelʳ-≡ : ∀ m n o .{{_ : NonZero o}} → m * o ≡ n * o → m ≡ n
-*-cancelʳ-≡ zero    zero    (suc o) eq = refl
-*-cancelʳ-≡ (suc m) (suc n) (suc o) eq =
-  cong suc (*-cancelʳ-≡ m n (suc o) (+-cancelˡ-≡ (suc o) (m * suc o) (n * suc o) eq))
+*-cancelʳ-≡ m n o = almost⇒exceptʳ _ _ *-almostCancelʳ-≡ (≢-nonZero⁻¹ _) m n
 
 *-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

src/Data/Rational/Properties.agda

@@ -13,7 +13,6 @@ open import Algebra.Apartness
 open import Algebra.Construct.NaturalChoice.Base
 import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp
 import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp
-open import Algebra.Consequences.Propositional
 open import Algebra.Morphism
 open import Algebra.Bundles
 import Algebra.Morphism.MagmaMonomorphism  as MagmaMonomorphisms
@@ -64,6 +63,7 @@ open import Relation.Nullary.Decidable.Core as Dec
   using (yes; no; recompute; map′; _×-dec_)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 
+open import Algebra.Consequences.Propositional {A = ℚ}
 open import Algebra.Definitions {A = ℚ} _≡_
 open import Algebra.Structures  {A = ℚ} _≡_
 
@@ -168,9 +168,9 @@ drop-*≡* (*≡* eq) = eq
       ℤ.∣ n₁ ∣ ℕ.* suc d₂    ∎)
 
   helper : mkℚ n₁ d₁ c₁ ≡ mkℚ n₂ d₂ c₂
-  helper with ∣-antisym 1+d₁∣1+d₂ 1+d₂∣1+d₁
-  ... | refl with ℤ.*-cancelʳ-≡ n₁ n₂ (+ suc d₁) eq
-  ...   | refl = refl
+  helper with refl ← ∣-antisym 1+d₁∣1+d₂ 1+d₂∣1+d₁
+         with refl ← ℤ.*-cancelʳ-≡ n₁ n₂ (+ suc d₁) eq
+    = refl
 
 ≃-sym : Symmetric _≃_
 ≃-sym = ≡⇒≃ ∘′ sym ∘′ ≃⇒≡
@@ -857,14 +857,14 @@ toℚᵘ-homo-+ p@record{} q@record{} with +-nf p q ℤ.≟ 0ℤ
   eq : ↥ (p + q) ≡ 0ℤ
   eq rewrite eq2 = cong ↥_ (0/n≡0 (↧ₙ p ℕ.* ↧ₙ q))
 
-... | no  nf[p,q]≢0 = *≡* (ℤ.*-cancelʳ-≡ _ _ (+-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} $ begin
+... | no  nf[p,q]≢0 = *≡* (ℤ.*-cancelʳ-≡ _ _ (+-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} (begin
     (↥ᵘ (toℚᵘ (p + q))) ℤ.* ↧+ᵘ p q  ℤ.* +-nf p q ≡⟨ cong (λ v → v ℤ.* ↧+ᵘ p q ℤ.* +-nf p q) (↥ᵘ-toℚᵘ (p + q)) ⟩
     ↥ (p + q) ℤ.* ↧+ᵘ p q ℤ.* +-nf p q            ≡⟨ xy∙z≈xz∙y (↥ (p + q)) _ _ ⟩
     ↥ (p + q) ℤ.* +-nf p q ℤ.* ↧+ᵘ p q            ≡⟨ cong (ℤ._* ↧+ᵘ p q) (↥-+ p q) ⟩
     ↥+ᵘ p q ℤ.* ↧+ᵘ p q                           ≡⟨ cong (↥+ᵘ p q ℤ.*_) (sym (↧-+ p q)) ⟩
     ↥+ᵘ p q ℤ.* (↧ (p + q) ℤ.* +-nf p q)          ≡⟨ x∙yz≈xy∙z (↥+ᵘ p q) _ _ ⟩
     ↥+ᵘ p q ℤ.* ↧ (p + q)  ℤ.* +-nf p q           ≡⟨ cong (λ v → ↥+ᵘ p q ℤ.* v ℤ.* +-nf p q) (↧ᵘ-toℚᵘ (p + q)) ⟨
-    ↥+ᵘ p q ℤ.* ↧ᵘ (toℚᵘ (p + q)) ℤ.* +-nf p q    ∎)
+    ↥+ᵘ p q ℤ.* ↧ᵘ (toℚᵘ (p + q)) ℤ.* +-nf p q    ∎))
   where open ≡-Reasoning; open CommSemigroupProperties ℤ.*-commutativeSemigroup
 
 toℚᵘ-isMagmaHomomorphism-+ : IsMagmaHomomorphism +-rawMagma ℚᵘ.+-rawMagma toℚᵘ
@@ -1092,14 +1092,14 @@ toℚᵘ-homo-* p@record{} q@record{} with *-nf p q ℤ.≟ 0ℤ
 
   eq : ↥ (p * q) ≡ 0ℤ
   eq rewrite eq2 = cong ↥_ (0/n≡0 (↧ₙ p ℕ.* ↧ₙ q))
-... | no nf[p,q]≢0 = *≡* (ℤ.*-cancelʳ-≡ _ _ (*-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} $ begin
+... | no nf[p,q]≢0 = *≡* (ℤ.*-cancelʳ-≡ _ _ (*-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} (begin
   ↥ᵘ (toℚᵘ (p * q)) ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q     ≡⟨ cong (λ v → v ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q) (↥ᵘ-toℚᵘ (p * q)) ⟩
   ↥ (p * q)         ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q     ≡⟨ xy∙z≈xz∙y (↥ (p * q)) _ _ ⟩
   ↥ (p * q)         ℤ.* *-nf p q ℤ.* (↧ p ℤ.* ↧ q)     ≡⟨ cong (ℤ._* (↧ p ℤ.* ↧ q)) (↥-* p q) ⟩
   (↥ p ℤ.* ↥ q)     ℤ.* (↧ p ℤ.* ↧ q)                  ≡⟨ cong ((↥ p ℤ.* ↥ q) ℤ.*_) (sym (↧-* p q)) ⟩
   (↥ p ℤ.* ↥ q)     ℤ.* (↧ (p * q) ℤ.* *-nf p q)       ≡⟨ x∙yz≈xy∙z (↥ p ℤ.* ↥ q) _ _ ⟩
   (↥ p ℤ.* ↥ q)     ℤ.* ↧ (p * q)  ℤ.* *-nf p q        ≡⟨ cong (λ v → (↥ p ℤ.* ↥ q) ℤ.* v ℤ.* *-nf p q) (↧ᵘ-toℚᵘ (p * q)) ⟨
-  (↥ p ℤ.* ↥ q)     ℤ.* ↧ᵘ (toℚᵘ (p * q)) ℤ.* *-nf p q ∎)
+  (↥ p ℤ.* ↥ q)     ℤ.* ↧ᵘ (toℚᵘ (p * q)) ℤ.* *-nf p q ∎))
   where open ≡-Reasoning; open CommSemigroupProperties ℤ.*-commutativeSemigroup
 
 toℚᵘ-homo-1/ : ∀ p .{{_ : NonZero p}} → toℚᵘ (1/ p) ℚᵘ.≃ (ℚᵘ.1/ toℚᵘ p)

src/Data/Rational/Unnormalised/Properties.agda

@@ -13,7 +13,6 @@ open import Algebra
 open import Algebra.Apartness
 open import Algebra.Lattice
 import Algebra.Consequences.Setoid as Consequences
-open import Algebra.Consequences.Propositional
 open import Algebra.Construct.NaturalChoice.Base
 import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp
 import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp
@@ -44,6 +43,7 @@ import Relation.Binary.Properties.Poset as PosetProperties
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 open import Relation.Binary.Reasoning.Syntax
 
+open import Algebra.Consequences.Propositional {A = ℚᵘ}
 open import Algebra.Properties.CommutativeSemigroup ℤ.*-commutativeSemigroup
 
 private
@@ -746,7 +746,7 @@ neg⇒nonZero (mkℚᵘ (-[1+ _ ]) _) = _
 +-identityˡ p = ≃-reflexive (+-identityˡ-≡ p)
 
 +-identityʳ-≡ : RightIdentity _≡_ 0ℚᵘ _+_
-+-identityʳ-≡ = comm+idˡ⇒idʳ +-comm-≡ {e = 0ℚᵘ} +-identityˡ-≡
++-identityʳ-≡ = comm∧idˡ⇒idʳ +-comm-≡ {e = 0ℚᵘ} +-identityˡ-≡
 
 +-identityʳ : RightIdentity _≃_ 0ℚᵘ _+_
 +-identityʳ p = ≃-reflexive (+-identityʳ-≡ p)
@@ -774,8 +774,8 @@ neg⇒nonZero (mkℚᵘ (-[1+ _ ]) _) = _
 +-inverse : Inverse _≃_ 0ℚᵘ -_ _+_
 +-inverse = +-inverseˡ , +-inverseʳ
 
-+-cancelˡ : ∀ {r p q} → r + p ≃ r + q → p ≃ q
-+-cancelˡ {r} {p} {q} r+p≃r+q = begin-equality
++-cancelˡ : LeftCancellative _≃_ _+_
++-cancelˡ r p q r+p≃r+q = begin-equality
   p            ≃⟨ +-identityʳ p ⟨
   p + 0ℚᵘ      ≃⟨ +-congʳ p (+-inverseʳ r) ⟨
   p + (r - r)  ≃⟨ +-assoc p r (- r) ⟨
@@ -787,12 +787,8 @@ neg⇒nonZero (mkℚᵘ (-[1+ _ ]) _) = _
   q + 0ℚᵘ      ≃⟨ +-identityʳ q ⟩
   q            ∎ where open ≤-Reasoning
 
-+-cancelʳ : ∀ {r p q} → p + r ≃ q + r → p ≃ q
-+-cancelʳ {r} {p} {q} p+r≃q+r = +-cancelˡ {r} $ begin-equality
-  r + p ≃⟨ +-comm r p ⟩
-  p + r ≃⟨ p+r≃q+r ⟩
-  q + r ≃⟨ +-comm q r ⟩
-  r + q ∎ where open ≤-Reasoning
++-cancelʳ : RightCancellative _≃_ _+_
++-cancelʳ = Consequences.comm∧cancelˡ⇒cancelʳ ≃-setoid +-comm +-cancelˡ
 
 p+p≃0⇒p≃0 : ∀ p → p + p ≃ 0ℚᵘ → p ≃ 0ℚᵘ
 p+p≃0⇒p≃0 (mkℚᵘ ℤ.+0 _) (*≡* _) = *≡* refl