[ fix ] CHANGELOG ahead of v2.4 (#2974)

* [ fix ] `CHANGELOG`

* fix: 'weird quotes', plus some more reordering

* fix: stupid unfolding of a definition in lemma statement

Author: jamesmckinna

CHANGELOG.md

@@ -67,10 +67,9 @@ Minor improvements
   `refl`, `sym`, and `trans` have been weakened to allow relations of different
   levels to be used.
 
-* Due to becoming large, `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties`
-  has been split into smaller modules
-  `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.*`
-  that are reexported by the original `Properties`.
+* The original `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties` has been
+  split up into smaller `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.*`
+  modules that are reexported by `Properties`.
 
 Deprecated modules
 ------------------
@@ -152,10 +151,6 @@ Deprecated names
 New modules
 -----------
 
-* Added tactic ring solvers for rational numbers (issue #1879):
-  `Data.Rational.Tactic.RingSolver`,
-  `Data.Rational.Unnormalised.Tactic.RingSolver`.
-
 * `Algebra.Construct.Sub.Group` for the definition of subgroups.
 
 * `Algebra.Module.Construct.Sub.Bimodule` for the definition of subbimodules.
@@ -170,12 +165,6 @@ New modules
 
 * `Data.List.Fresh.Membership.DecSetoid`.
 
-* `Data.List.Relation.Binary.Permutation.Algorithmic{.Properties}` for the Choudhury and Fiore definition of permutation, and its equivalence with `Declarative` below.
-
-* `Data.List.Relation.Binary.Permutation.Declarative{.Properties}` for the least congruence on `List` making `_++_` commutative, and its equivalence with the `Setoid` definition.
-
-* `Effect.Monad.Random` and `Effect.Monad.Random.Instances` for an mtl-style randomness monad constraint.
-
 * Various additions over non-empty lists:
   ```
   Data.List.NonEmpty.Relation.Binary.Pointwise
@@ -184,6 +173,16 @@ New modules
   Data.List.NonEmpty.Membership.Setoid
   ```
 
+* `Data.List.Relation.Binary.Permutation.Algorithmic{.Properties}` for the Choudhury and Fiore definition of permutation, and its equivalence with `Declarative` below.
+
+* `Data.List.Relation.Binary.Permutation.Declarative{.Properties}` for the least congruence on `List` making `_++_` commutative, and its equivalence with the `Setoid` definition.
+
+* Added tactic ring solvers for rational numbers (issue #1879):
+  ```agda
+  Data.Rational.Tactic.RingSolver
+  Data.Rational.Unnormalised.Tactic.RingSolver
+  ```
+
 * Refactoring of `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties` as smaller modules:
   ```
   Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Lookup
@@ -196,6 +195,8 @@ New modules
   Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Singleton
   ```
 
+* `Effect.Monad.Random` and `Effect.Monad.Random.Instances` for an mtl-style randomness monad constraint.
+
 * `Relation.Binary.Morphism.Construct.On`: given a relation `_∼_` on `B`,
   and a function `f : A → B`, construct the canonical `IsRelMonomorphism`
   between `_∼_ on f` and `_∼_`, witnessed by `f` itself.
@@ -355,7 +356,7 @@ Additions to existing modules
 
   ≲%[o]⇒≡[o]% : .{{_ : NonZero o}} → _≲%[ o ]_ ⇒ _≡%[ o ]_
   ≅%[o]⇒≡[o]% : .{{_ : NonZero o}} → _≅%[ o ]_ ⇒ _≡%[ o ]_
-  ≡[o]%⇒≲%[o] : .{{_ : NonZero o}} → m % o ≡ n % o → m ≤ n → m ≲%[ o ] n
+  ≡[o]%⇒≲%[o] : .{{_ : NonZero o}} → m ≡%[ o ] n → m ≤ n → m ≲%[ o ] n
   ≡[o]%⇒≅%[o] : .{{_ : NonZero o}} → _≡%[ o ]_ ⇒ _≅%[ o ]_
 
   ≡%-suc-injective : .{{_ : NonZero o}} → Injective _≡%[ o ]_ _≡%[ o ]_ suc
@@ -595,6 +596,19 @@ Additions to existing modules
                       padRight m≤n x (updateAt xs i f)
   ```
 
+* In `Data.Vec.Relation.Binary.Pointwise.Inductive`
+  ```agda
+  irrelevant : ∀ {_∼_ : REL A B ℓ} {n m} → Irrelevant _∼_ → Irrelevant (Pointwise _∼_ {n} {m})
+  antisym : ∀ {P : REL A B ℓ₁} {Q : REL B A ℓ₂} {R : REL A B ℓ} {m n} →
+            Antisym P Q R → Antisym (Pointwise P {m}) (Pointwise Q {n}) (Pointwise R)
+  ```
+
+* In `Data.Vec.Relation.Binary.Pointwise.Extensional`
+  ```agda
+  antisym : ∀ {P : REL A B ℓ₁} {Q : REL B A ℓ₂} {R : REL A B ℓ} {n} →
+            Antisym P Q R → Antisym (Pointwise P {n}) (Pointwise Q) (Pointwise R)
+  ```
+
 * In `Relation.Binary.Construct.Add.Extrema.NonStrict`:
   ```agda
   ≤±-respˡ-≡ : _≤±_ Respectsˡ _≡_
@@ -633,19 +647,6 @@ Additions to existing modules
   on⁻  : SymClosure (R on g) ⇒ ((SymClosure R) on g)
   ```
 
-* In `Data.Vec.Relation.Binary.Pointwise.Inductive`
-  ```agda
-  irrelevant : ∀ {_∼_ : REL A B ℓ} {n m} → Irrelevant _∼_ → Irrelevant (Pointwise _∼_ {n} {m})
-  antisym : ∀ {P : REL A B ℓ₁} {Q : REL B A ℓ₂} {R : REL A B ℓ} {m n} →
-            Antisym P Q R → Antisym (Pointwise P {m}) (Pointwise Q {n}) (Pointwise R)
-  ```
-
-* In `Data.Vec.Relation.Binary.Pointwise.Extensional`
-  ```agda
-  antisym : ∀ {P : REL A B ℓ₁} {Q : REL B A ℓ₂} {R : REL A B ℓ} {n} →
-            Antisym P Q R → Antisym (Pointwise P {n}) (Pointwise Q) (Pointwise R)
-  ```
-
 * In `Relation.Binary.Properties.Setoid`:
   ```agda
   ¬[x≉x] : .(x ≉ x) → Whatever
@@ -678,20 +679,16 @@ Additions to existing modules
   ⟨_⟩⊢⁺_    : P ⊆ f ⊢ Q → ⟨ f ⟩⊢ P ⊆ Q
   [_]⊢⁻_    : Q ⊆ [ f ]⊢ P → f ⊢ Q ⊆ P
   [_]⊢⁺_    : f ⊢ Q ⊆ P → Q ⊆ [ f ]⊢ P
-  ```
-
-* In `System.Random`:
-  ```agda
-  randomIO : IO Bool
-  randomRIO : RandomRIO {A = Bool} _≤_
-  ```
-
-* In Relation.Unary.Properites
-  ```agda
   ¬∃⟨P⟩⇒Π[∁P] : ¬ ∃⟨ P ⟩ → Π[ ∁ P ]
   ¬∃⟨P⟩⇒∀[∁P] : ¬ ∃⟨ P ⟩ → ∀[ ∁ P ]
   ∃⟨∁P⟩⇒¬Π[P] : ∃⟨ ∁ P ⟩ → ¬ Π[ P ]
   ∃⟨∁P⟩⇒¬∀[P] : ∃⟨ ∁ P ⟩ → ¬ ∀[ P ]
   Π[∁P]⇒¬∃[P] : Π[ ∁ P ] → ¬ ∃⟨ P ⟩
   ∀[∁P]⇒¬∃[P] : ∀[ ∁ P ] → ¬ ∃⟨ P ⟩
   ```
+
+* In `System.Random`:
+  ```agda
+  randomIO : IO Bool
+  randomRIO : RandomRIO {A = Bool} _≤_
+  ```

src/Data/Nat/DivMod.agda

@@ -496,7 +496,7 @@ module _ .{{_ : NonZero o}} where
   ≅%[o]⇒≡[o]% : _≅%[ o ]_ ⇒ _≡%[ o ]_
   ≅%[o]⇒≡[o]% = SymClosure.fold sym ≲%[o]⇒≡[o]%
 
-  ≡[o]%⇒≲%[o] : m % o ≡ n % o → m ≤ n → m ≲%[ o ] n
+  ≡[o]%⇒≲%[o] : m ≡%[ o ] n → m ≤ n → m ≲%[ o ] n
   ≡[o]%⇒≲%[o] {m = m} {n = n} eq m≤n = k , (begin-equality
     n                           ≡⟨ m≡m%n+[m/n]*n n o ⟩
     n % o + n / o * o           ≡⟨ cong (_+ n / o * o) eq ⟨