move Qp changelogs entries together, and remove outdated ones

CHANGELOG.md

@@ -7,15 +7,14 @@ Coq 8.8 and 8.9 are no longer supported.
 
 - Rename `dom_map filter` → `dom_filter`, `dom_map_filter_L` → `dom_filter_L`,
   and `dom_map_filter_subseteq` → `dom_filter_subseteq` for consistency's sake.
-- Add `max` and `min` operations for `Qp`.
-- Add additional lemmas for `Qp`.
-- Remove the lemma `Qp_not_plus_q_ge_1` in favor of `Qp_not_plus_ge`.
 - Remove unused notations `∪**`, `∪*∪**`, `∖**`, `∖*∖**`, `⊆**`, `⊆1*`, `⊆2*`,
   `⊆1**`, `⊆2**"`, `##**`, `##1*`, `##2*`, `##1**`, `##2**` for nested
   `zip_with` and `Forall2` versions of `∪`, `∖`, and `##`.
 - Remove unused type classes `DisjointE`, `DisjointList`, `LookupE`, and
   `InsertE`.
 - Overhaul of the theory of positive rationals `Qp`:
+  + Add `max` and `min` operations for `Qp`.
+  + Add additional lemmas for `Qp`.
   + Add the orders `Qp_le` and `Qp_lt`.
   + Rename `Qp_plus` into `Qp_add` and `Qp_mult` into `Qp_mul` to be consistent
     with the corresponding names for `nat`, `N`, and `Z`.