diff --git a/OrderedSemigroups/Archimedean.lean b/OrderedSemigroups/Archimedean.lean
index 2d79182..1a465f8 100644
--- a/OrderedSemigroups/Archimedean.lean
+++ b/OrderedSemigroups/Archimedean.lean
@@ -15,27 +15,29 @@ variable {α : Type u}
 section OrderedSemigroup
 variable [OrderedSemigroup α]
 
+/-- `a` is Archimedean with respect to `b` if there exists an `N : ℕ+` such that
+for all `n ≥ N`, either `b` is positive and `b < a^n` or `b` is negative and `a^n < b`. -/
 abbrev is_archimedean_wrt (a b : α) :=
   ∃N : ℕ+, ∀n : ℕ+, n ≥ N → (is_positive b ∧ b < a^n) ∨ (is_negative b ∧ a^n < b)
 
+/-- A pair of elements `a` and `b` form an anomalous pair if for all `n : ℕ+`,
+either `a^n < b^n` and `b^n < a^(n+1)` or `a^n > b^n` and `b^n > a^(n+1)`. -/
 abbrev anomalous_pair (a b : α) := ∀n : ℕ+, (a^n < b^n ∧ b^n < a^(n+1)) ∨ (a^n > b^n ∧ b^n > a^(n+1))
 
+/-- An ordered semigroup has an anomalous pair if there exist elements `a` and `b` such that
+`a` and `b` form an anomalous pair. -/
 abbrev has_anomalous_pair := ∃a b : α, anomalous_pair a b
 
+/-- An ordered semigroup is Archimedean if for all elements `a` and `b` of it, either
+`a` is one, `b` is one, or if `a` and `b` have the same sign, then `a` is Archimedean with respect to `b`.-/
 def is_archimedean := ∀a b : α, is_one a ∨ is_one b ∨ (same_sign a b → is_archimedean_wrt a b)
 
-class Archimedean (α : Type u) [OrderedSemigroup α] where
-  arch : is_archimedean (α := α)
-
-theorem not_has_anomalous_not_pair (not_anomalous : ¬has_anomalous_pair (α := α)) (a b : α) : ¬anomalous_pair a b := by
-  simp at *
-  tauto
-
 end OrderedSemigroup
 
 section LinearOrderedCancelSemigroup
 variable [LinearOrderedCancelSemigroup α]
 
+/-- If `a` is Archimedean with respect to `b`, then `a` and `b` have the same sign. -/
 theorem archimedean_same_sign {a b : α} (arch : is_archimedean_wrt a b) : same_sign a b := by
   obtain ⟨N, arch⟩ := arch
   rcases arch N (by simp) with ⟨pos_b, h⟩ | ⟨neg_b , h⟩
@@ -49,6 +51,7 @@ theorem archimedean_same_sign {a b : α} (arch : is_archimedean_wrt a b) : same_
     · exact pow_le_neg_neg neg_b N h.le
     · trivial
 
+/-- If `b` is positive and there exists an `n : ℕ+` such that `a^n ≥ b`, then `a` is Archimedean with respect to `b`. -/
 theorem pos_ge_once_archimedean {a b : α} (pos : is_positive b) (h : ∃n : ℕ+, a^n ≥ b) : is_archimedean_wrt a b := by
   rcases h with ⟨n, hn⟩
   use n+1
@@ -58,6 +61,7 @@ theorem pos_ge_once_archimedean {a b : α} (pos : is_positive b) (h : ∃n : ℕ
   · trivial
   · exact lt_of_le_of_lt hn (pos_ppow_lt_ppow n x (pos_le_pow_pos pos n hn) hx)
 
+/-- If `b` is negative and there exists an `n : ℕ+` such that `a^n ≤ b`, then `a` is Archimedean with respect to `b`. -/
 theorem neg_ge_once_archimedean {a b : α} (neg : is_negative b) (h : ∃n : ℕ+, a^n ≤ b) : is_archimedean_wrt a b := by
   rcases h with ⟨n, hn⟩
   use n+1
@@ -67,16 +71,19 @@ theorem neg_ge_once_archimedean {a b : α} (neg : is_negative b) (h : ∃n : ℕ
   · trivial
   · exact gt_of_ge_of_gt hn (neg_ppow_lt_ppow n x (pow_le_neg_neg neg n hn) hx)
 
+/-- If `b` is positive and `a` is not Archimedean with respect to `b`, then for all `n : ℕ+`, `a^n < b`. -/
 theorem pos_not_archimedean_wrt_forall_lt {a b : α} (pos : is_positive b) (h : ¬is_archimedean_wrt a b) :
     ∀n : ℕ+, a^n < b := by
   have := mt (pos_ge_once_archimedean pos) h
   simpa
 
+/-- If `b` is negative and `a` is not Archimedean with respect to `b`, then for all `n : ℕ+`, `b < a^n`. -/
 theorem neg_not_archimedean_wrt_forall_gt {a b : α} (neg : is_negative b) (h : ¬is_archimedean_wrt a b) :
     ∀n : ℕ+, b < a^n := by
   have := mt (neg_ge_once_archimedean neg) h
   simpa
 
+/-- If `a` and `b` are positive, `a` is not Archimedean with respect to `b`, and `a*b ≤ b*a`, then `b` and `a*b` form an anomalous pair. -/
 theorem pos_not_arch_anomalous_pair {a b : α} (pos_a : is_positive a) (pos_b : is_positive b)
     (not_arch : ¬is_archimedean_wrt a b) (comm : a*b ≤ b*a) : anomalous_pair b (a*b) := by
   intro n
@@ -89,6 +96,7 @@ theorem pos_not_arch_anomalous_pair {a b : α} (pos_a : is_positive a) (pos_b :
       _           < b ^ n * b := mul_lt_mul_left' (pos_not_archimedean_wrt_forall_lt pos_b not_arch n) (b ^ n)
       _           = b ^ (n + 1) := Eq.symm (ppow_succ n b)
 
+/-- If `a` and `b` are positive, `a` is not Archimedean with respect to `b`, and `b*a ≤ a*b`, then `b` and `a*b` form an anomalous pair. -/
 theorem pos_not_arch_anomalous_pair' {a b : α} (pos_a : is_positive a) (pos_b : is_positive b)
     (not_arch : ¬is_archimedean_wrt a b) (comm : b*a ≤ a*b) : anomalous_pair b (a*b) := by
   intro n
@@ -103,6 +111,7 @@ theorem pos_not_arch_anomalous_pair' {a b : α} (pos_a : is_positive a) (pos_b :
       _           < b * b ^ n := mul_lt_mul_right' (pos_not_archimedean_wrt_forall_lt pos_b not_arch n) (b ^ n)
       _           = b ^ (n + 1) := Eq.symm (ppow_succ' n b)
 
+/-- If `a` and `b` are negative, `a` is not Archimedean with respect to `b`, and `a*b ≤ b*a`, then `b` and `a*b` form an anomalous pair. -/
 theorem neg_not_archimedean_anomalous_pair {a b : α} (neg_a : is_negative a) (neg_b : is_negative b)
     (not_arch : ¬is_archimedean_wrt a b) (comm : a*b ≤ b*a) : anomalous_pair b (a*b) := by
   intro n
@@ -117,6 +126,7 @@ theorem neg_not_archimedean_anomalous_pair {a b : α} (neg_a : is_negative a) (n
       _           > b * b ^ n := mul_lt_mul_right' (neg_not_archimedean_wrt_forall_gt neg_b not_arch n ) (b ^ n)
       _           = b ^ (n + 1) := Eq.symm (ppow_succ' n b)
 
+/-- If `a` and `b` are negative, `a` is not Archimedean with respect to `b`, and `b*a ≤ a*b`, then `b` and `a*b` form an anomalous pair. -/
 theorem neg_not_archimedean_anomalous_pair' {a b : α} (neg_a : is_negative a) (neg_b : is_negative b)
     (not_arch : ¬is_archimedean_wrt a b) (comm : b*a ≤ a*b) : anomalous_pair b (a*b) := by
   intro n
@@ -129,6 +139,7 @@ theorem neg_not_archimedean_anomalous_pair' {a b : α} (neg_a : is_negative a) (
       _           > b ^ n * b := mul_lt_mul_left' (neg_not_archimedean_wrt_forall_gt neg_b not_arch n) (b ^ n)
       _           = b ^ (n + 1) := Eq.symm (ppow_succ n b)
 
+/-- If a linear ordered cancel semigroup is not Archimedean, then it has an anomalous pair. -/
 theorem non_archimedean_anomalous_pair (non_arch : ¬is_archimedean (α := α)) : has_anomalous_pair (α := α) := by
   unfold is_archimedean at non_arch
   push_neg at non_arch
@@ -147,6 +158,7 @@ theorem non_archimedean_anomalous_pair (non_arch : ¬is_archimedean (α := α))
     · exact neg_not_archimedean_anomalous_pair neg_a neg_b hab h
     · exact neg_not_archimedean_anomalous_pair' neg_a neg_b hab h
 
+/-- If `a` and `b` are positive and `a * b < b * a`, then `a*b` and `b*a` form an anomalous pair. -/
 theorem pos_not_comm_anomalous_pair {a b : α} (pos_a : is_positive a) (pos_b : is_positive b)
     (h : a * b < b * a) : anomalous_pair (a*b) (b*a) := by
   intro n
@@ -159,6 +171,7 @@ theorem pos_not_comm_anomalous_pair {a b : α} (pos_a : is_positive a) (pos_b :
   left
   exact ⟨comm_swap_lt h n, this n⟩
 
+/-- If `a` and `b` are negative and `a * b < b * a`, then `b*a` and `a*b` form an anomalous pair. -/
 theorem neg_not_comm_anomalous_pair {a b : α} (neg_a : is_negative a) (neg_b : is_negative b)
     (h : a * b < b * a) : anomalous_pair (b*a) (a*b) := by
   intro n
@@ -171,6 +184,7 @@ theorem neg_not_comm_anomalous_pair {a b : α} (neg_a : is_negative a) (neg_b :
   right
   exact ⟨comm_swap_lt h n, this n⟩
 
+/-- If `a` and `b` are positive and there is no anomalous pair, then `a` and `b` commute. -/
 theorem pos_not_anomalous_comm {a b : α} (pos_a : is_positive a) (pos_b : is_positive b)
     (not_anomalous : ¬has_anomalous_pair (α := α)): a * b = b * a := by
   rcases lt_trichotomy (a*b) (b*a) with h | h | h
@@ -184,6 +198,7 @@ theorem pos_not_anomalous_comm {a b : α} (pos_a : is_positive a) (pos_b : is_po
       exact pos_not_comm_anomalous_pair pos_b pos_a h
     contradiction
 
+/-- If `a` and `b` are negative and there is no anomalous pair, then `a` and `b` commute. -/
 theorem neg_not_anomalous_comm {a b : α} (neg_a : is_negative a) (neg_b : is_negative b)
     (not_anomalous : ¬has_anomalous_pair (α := α)): a * b = b * a := by
   rcases lt_trichotomy (a*b) (b*a) with h | h | h
@@ -197,6 +212,51 @@ theorem neg_not_anomalous_comm {a b : α} (neg_a : is_negative a) (neg_b : is_ne
       exact neg_not_comm_anomalous_pair neg_b neg_a h
     contradiction
 
+/-- If `a * b < b * a` and `(b * a)` commutes with `b`, then we have a contradiction and so `a` and `b` commute. -/
+theorem not_comm_once_comm {a b : α} (h : a * b < b * a) (comm : (b * a) * b = b * (b * a)) :
+  a * b = b * a := by
+  have : a * b * a * b > a * b * a * b := calc
+    a * b * a * b = a * ((b * a) * b) := by simp [mul_assoc]
+    _             = a * (b * (b * a)) := by simp [←comm]
+    _             = (a * b) * (b * a) := by simp [mul_assoc]
+    _             > (a * b) * (a * b) := by exact mul_lt_mul_left' h (a * b)
+    _             = a * b * a * b := by exact Eq.symm (mul_assoc (a * b) a b)
+  exact False.elim ((lt_self_iff_false (a * b * a * b)).mp this)
+
+/-- If `b * a < a * b` and `(b * a)` commutes with `b`, then we have a contradiction and so `a` and `b` commute. -/
+theorem not_comm_once_comm' {a b : α} (h : b * a < a * b) (comm : (b * a) * b = b * (b * a)) :
+  a * b = b * a := by
+  have : a * b * a * b > a * b * a * b := calc
+    a * b * a * b = a * ((b * a) * b) := by simp [mul_assoc]
+    _             = a * (b * (b * a)) := by simp [←comm]
+    _             = (a * b) * (b * a) := by simp [mul_assoc]
+    _             < (a * b) * (a * b) := by exact mul_lt_mul_left' h (a * b)
+    _             = a * b * a * b := by exact Eq.symm (mul_assoc (a * b) a b)
+  exact False.elim ((lt_self_iff_false (a * b * a * b)).mp this)
+
+/-- If `a * b < b * a` and `(b * a)` commutes with `a`, then we have a contradiction and so `a` and `b` commute. -/
+theorem not_comm_once_comm'' {a b : α} (h : a * b < b * a) (comm : (b * a) * a = a * (b * a)) :
+  a * b = b * a := by
+  have : a * b * a * b > a * b * a * b := calc
+    a * b * a * b = (a * (b * a)) * b := by simp [mul_assoc]
+    _             = ((b * a) * a) * b := by simp [←comm]
+    _             = (b * a) * (a * b) := by simp [mul_assoc]
+    _             > (a * b) * (a * b) := by exact mul_lt_mul_right' h (a * b)
+    _             = a * b * a * b := by exact Eq.symm (mul_assoc (a * b) a b)
+  exact False.elim ((lt_self_iff_false (a * b * a * b)).mp this)
+
+/-- If `b * a < a * b` and `(b * a)` commutes with `a`, then we have a contradiction and so `a` and `b` commute. -/
+theorem not_comm_once_comm''' {a b : α} (h : b * a < a * b) (comm : (b * a) * a = a * (b * a)) :
+  a * b = b * a := by
+  have : a * b * a * b > a * b * a * b := calc
+    a * b * a * b = (a * (b * a)) * b := by simp [mul_assoc]
+    _             = ((b * a) * a) * b := by simp [←comm]
+    _             = (b * a) * (a * b) := by simp [mul_assoc]
+    _             < (a * b) * (a * b) := by exact mul_lt_mul_right' h (a * b)
+    _             = a * b * a * b := by exact Eq.symm (mul_assoc (a * b) a b)
+  exact False.elim ((lt_self_iff_false (a * b * a * b)).mp this)
+
+/-- If a linear ordered cancel semigroup does not have an anomalous pair, then it is commutative. -/
 theorem not_anomalous_pair_commutative (not_anomalous : ¬has_anomalous_pair (α := α)) (a b : α) : a * b = b * a := by
   rcases pos_neg_or_one a with pos_a | neg_a | one_a
   <;> rcases pos_neg_or_one b with pos_b | neg_b | one_b
@@ -204,8 +264,16 @@ theorem not_anomalous_pair_commutative (not_anomalous : ¬has_anomalous_pair (α
   all_goals try simp [one_a b, one_right one_a b]
   · exact pos_not_anomalous_comm pos_a pos_b not_anomalous
   · rcases pos_neg_or_one (a*b) with pos_ab | neg_ab | one_ab
-    · sorry
-    · sorry
+    have := pos_not_anomalous_comm pos_ab pos_a not_anomalous
+    · rcases lt_trichotomy (a*b) (b*a) with h | h | h
+      · exact Eq.symm (not_comm_once_comm' h this)
+      · trivial
+      · exact Eq.symm (not_comm_once_comm h this)
+    have := neg_not_anomalous_comm neg_ab neg_b not_anomalous
+    · rcases lt_trichotomy (a*b) (b*a) with h | h | h
+      · exact Eq.symm (not_comm_once_comm''' h this)
+      · trivial
+      · exact Eq.symm (not_comm_once_comm'' h this)
     · have : is_one (b * a) := by
         apply one_right_one_forall (b := a)
         rw [Eq.symm (mul_assoc a b a)]
@@ -214,22 +282,14 @@ theorem not_anomalous_pair_commutative (not_anomalous : ¬has_anomalous_pair (α
   · rcases pos_neg_or_one (b*a) with pos_ba | neg_ba | one_ba
     have := pos_not_anomalous_comm pos_ba pos_b not_anomalous
     · rcases lt_trichotomy (a*b) (b*a) with h | h | h
-      · have : a * b * a * b > a * b * a * b := calc
-          a * b * a * b = a * ((b * a) * b) := by simp [mul_assoc]
-          _             = a * (b * (b * a)) := by simp [←this]
-          _             = (a * b) * (b * a) := by simp [mul_assoc]
-          _             > (a * b) * (a * b) := by exact mul_lt_mul_left' h (a * b)
-          _             = a * b * a * b := by exact Eq.symm (mul_assoc (a * b) a b)
-        exact False.elim ((lt_self_iff_false (a * b * a * b)).mp this)
+      · exact not_comm_once_comm h this
+      · trivial
+      · exact not_comm_once_comm' h this
+    have := neg_not_anomalous_comm neg_ba neg_a not_anomalous
+    · rcases lt_trichotomy (a*b) (b*a) with h | h | h
+      · exact not_comm_once_comm'' h this
       · trivial
-      · have : a * b * a * b > a * b * a * b := calc
-          a * b * a * b = a * ((b * a) * b) := by simp [mul_assoc]
-          _             = a * (b * (b * a)) := by simp [←this]
-          _             = (a * b) * (b * a) := by simp [mul_assoc]
-          _             < (a * b) * (a * b) := by exact mul_lt_mul_left' h (a * b)
-          _             = a * b * a * b := by exact Eq.symm (mul_assoc (a * b) a b)
-        exact False.elim ((lt_self_iff_false (a * b * a * b)).mp this)
-    · sorry
+      · exact not_comm_once_comm''' h this
     · have : is_one (a * b) := by
         apply one_right_one_forall (b := b)
         rw [Eq.symm (mul_assoc b a b)]
diff --git a/OrderedSemigroups/Basic.lean b/OrderedSemigroups/Basic.lean
index 70814a0..ffe7e03 100644
--- a/OrderedSemigroups/Basic.lean
+++ b/OrderedSemigroups/Basic.lean
@@ -103,16 +103,4 @@ theorem lt_pow {a b : α} (h : a < b) (n : ℕ+) : a^n < b^n := by
 
 theorem comm_swap_lt {a b : α} (h : a*b < b*a) (n : ℕ+) : (a*b)^n < (b*a)^n := lt_pow h n
 
-/-
-theorem comm_dist_lt {a b : α} (h : a*b < b*a) (n : ℕ+) : n > 1 → (b*a)^n < b^n * a^n := by
-  induction n using PNat.recOn with
-  | p1 => intro; contradiction
-  | hp n ih =>
-    calc
-      (b*a)^(n+1) = b * (a*b)^n * a := by rw [split_first_and_last_factor_of_product]
-      _           ≤ b * (b*a)^n * a := middle_swap (le_pow h n)
-      _           ≤ b * (b^n * a^n) * a := middle_swap ih
-      _           = (b * b^n) * (a^n * a) := by simp [mul_assoc]
-      _           = b^(n+1) * a^(n+1) := by simp [ppow_succ, ←ppow_succ']-/
-
 end OrderedCancelSemigroup
diff --git a/OrderedSemigroups/PNat.lean b/OrderedSemigroups/PNat.lean
index a34bdef..4d136d3 100644
--- a/OrderedSemigroups/PNat.lean
+++ b/OrderedSemigroups/PNat.lean
@@ -1,5 +1,13 @@
 import Mathlib.Data.PNat.Basic
 
+/-!
+# Positive Naturals
+
+This file proves some basic lemmas about `PNat` (aka `ℕ+`)
+that are used in relation to exponentiation of elements in a semigroup.
+
+-/
+
 lemma add_sub_eq (x y : ℕ+) : x + y - y = x := by
   apply PNat.eq
   simp [PNat.sub_coe, PNat.lt_add_left y x]