diff --git a/DuperOnMathlib/DuperOnMathlib/MIL/C03_Logic/S03_Negation.lean b/DuperOnMathlib/DuperOnMathlib/MIL/C03_Logic/S03_Negation.lean
new file mode 100644
index 0000000..67836c6
--- /dev/null
+++ b/DuperOnMathlib/DuperOnMathlib/MIL/C03_Logic/S03_Negation.lean
@@ -0,0 +1,168 @@
+import Mathlib.Data.Real.Basic
+import Duper.Tactic
+
+namespace C03S03
+
+section
+variable (a b : ℝ)
+
+example (h : a < b) : ¬b < a := by
+  intro h'
+  have : a < a := lt_trans h h'
+  apply lt_irrefl a this
+
+example (h : a < b) : ¬b < a := by
+  duper [lt_trans, lt_irrefl, *]
+
+def FnUb (f : ℝ → ℝ) (a : ℝ) : Prop :=
+  ∀ x, f x ≤ a
+
+def FnLb (f : ℝ → ℝ) (a : ℝ) : Prop :=
+  ∀ x, a ≤ f x
+
+def FnHasUb (f : ℝ → ℝ) :=
+  ∃ a, FnUb f a
+
+def FnHasLb (f : ℝ → ℝ) :=
+  ∃ a, FnLb f a
+
+variable (f : ℝ → ℝ)
+
+example (h : ∀ a, ∃ x, f x > a) : ¬FnHasUb f := by
+  intro fnub
+  rcases fnub with ⟨a, fnuba⟩
+  rcases h a with ⟨x, hx⟩
+  have : f x ≤ a := fnuba x
+  linarith
+
+example (h : ∀ a, ∃ x, f x > a) : ¬FnHasUb f := by
+ duper [*, FnHasUb, FnUb, gt_iff_lt, not_le]
+
+example (h : ∀ a, ∃ x, f x < a) : ¬FnHasLb f := by
+ duper [*, FnHasLb, FnLb, gt_iff_lt, not_le]
+
+example : ¬FnHasUb fun x ↦ x := by
+  have : ∀ x : ℝ, x < x + 1  := by simp
+  duper [*, FnHasUb, FnUb, gt_iff_lt, not_le, this]
+
+#check (not_le_of_gt : a > b → ¬a ≤ b)
+#check (not_lt_of_ge : a ≥ b → ¬a < b)
+#check (lt_of_not_ge : ¬a ≥ b → a < b)
+#check (le_of_not_gt : ¬a > b → a ≤ b)
+
+
+example (h : Monotone f) (h' : f a < f b) : a < b := by
+  apply lt_of_not_ge
+  intro h''
+  apply absurd h'
+  apply not_lt_of_ge (h h'')
+
+-- Nice!
+example (h : Monotone f) (h' : f a < f b) : a < b := by
+  duper [lt_of_not_ge, not_lt_of_ge, Monotone, *]
+
+example (h : a ≤ b) (h' : f b < f a) : ¬Monotone f := by
+  intro h''
+  apply absurd h'
+  apply not_lt_of_ge
+  apply h'' h
+
+example (h : a ≤ b) (h' : f b < f a) : ¬Monotone f := by
+  duper [Monotone, not_lt_of_ge, *]
+
+example : ¬∀ {f : ℝ → ℝ}, Monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := by
+  intro h
+  let f := fun x : ℝ ↦ (0 : ℝ)
+  have monof : Monotone f := by
+    intro a b leab
+    rfl
+  have h' : f 1 ≤ f 0 := le_refl _
+  have : (1 : ℝ) ≤ 0 := h monof h'
+  linarith
+
+example : ¬∀ {f : ℝ → ℝ}, Monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := by
+    set f := fun x : ℝ ↦ (0 : ℝ) with hf
+    have h' : f 1 ≤ f 0 := le_refl _
+    have : ¬ (1 : ℝ ) ≤ 0 := by linarith
+    duper [Monotone, *]
+
+example (x : ℝ) (h : ∀ ε > 0, x < ε) : x ≤ 0 := by
+  apply le_of_not_gt
+  intro h'
+  linarith [h _ h']
+
+example (x : ℝ) (h : ∀ ε > 0, x < ε) : x ≤ 0 := by
+  duper [*, le_of_not_gt, lt_irrefl]
+
+end
+
+section
+variable {α : Type*} (P : α → Prop) (Q : Prop)
+
+example (h : ¬∃ x, P x) : ∀ x, ¬P x := by
+  duper [h]
+
+example (h : ∀ x, ¬P x) : ¬∃ x, P x := by
+  duper [h]
+
+example (h : ¬∀ x, P x) : ∃ x, ¬P x := by
+  duper [h]
+
+example (h : ∃ x, ¬P x) : ¬∀ x, P x := by
+  duper [h]
+
+example (h : ¬¬Q) : Q := by
+  duper [h]
+
+example (h : Q) : ¬¬Q := by
+  duper [h]
+
+end
+
+section
+variable (f : ℝ → ℝ)
+
+example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
+  intro a
+  by_contra h'
+  apply h
+  use a
+  intro x
+  apply le_of_not_gt
+  intro h''
+  apply h'
+  use x
+
+example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
+  duper [h, le_of_not_gt, FnHasUb, FnUb]
+
+example (h : ¬∀ a, ∃ x, f x > a) : FnHasUb f := by
+  push_neg at h
+  exact h
+
+example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
+  dsimp only [FnHasUb, FnUb] at h
+  push_neg at h
+  exact h
+
+example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
+  duper [FnHasUb, FnUb, h, le_of_not_gt]
+
+example (h : ¬Monotone f) : ∃ x y, x ≤ y ∧ f y < f x := by
+  duper [Monotone, h, le_of_not_gt]
+
+
+example (x : ℝ) (h : ∀ ε > 0, x ≤ ε) : x ≤ 0 := by
+  contrapose! h
+  use x / 2
+  constructor <;> linarith
+
+end
+
+section
+variable (a : ℕ)
+
+example (h : 0 < 0) : a > 37 := by
+  duper [h, lt_irrefl]
+
+end
diff --git a/DuperOnMathlib/DuperOnMathlib/MIL/C03_Logic/S04_Conjunction_and_Iff.lean b/DuperOnMathlib/DuperOnMathlib/MIL/C03_Logic/S04_Conjunction_and_Iff.lean
new file mode 100644
index 0000000..85780ed
--- /dev/null
+++ b/DuperOnMathlib/DuperOnMathlib/MIL/C03_Logic/S04_Conjunction_and_Iff.lean
@@ -0,0 +1,167 @@
+import Mathlib.Data.Real.Basic
+import Mathlib.Data.Nat.Prime
+import Duper.Tactic
+
+namespace C03S04
+
+example {x y : ℝ} (h₀ : x ≤ y) (h₁ : ¬y ≤ x) : x ≤ y ∧ x ≠ y := by
+  duper [*]
+
+example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
+  duper [*, le_antisymm]
+
+example {m n : ℕ} (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬n ∣ m := by
+  rcases h with ⟨h0, h1⟩
+  constructor
+  · exact h0
+  intro h2
+  apply h1
+  apply Nat.dvd_antisymm h0 h2
+
+example {m n : ℕ} (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬n ∣ m := by
+  duper [*, Nat.dvd_antisymm]
+
+example : ∃ x : ℝ, 2 < x ∧ x < 4 :=
+  ⟨5 / 2, by norm_num, by norm_num⟩
+
+example (x y : ℝ) : (∃ z : ℝ, x < z ∧ z < y) → x < y := by
+  rintro ⟨z, xltz, zlty⟩
+  exact lt_trans xltz zlty
+
+example (x y : ℝ) : (∃ z : ℝ, x < z ∧ z < y) → x < y := by
+  duper [*, lt_trans]
+
+example : ∃ m n : ℕ, 4 < m ∧ m < n ∧ n < 10 ∧ Nat.Prime m ∧ Nat.Prime n := by
+  use 5
+  use 7
+  norm_num
+
+example : ∃ m n : ℕ, 4 < m ∧ m < n ∧ n < 10 ∧ Nat.Prime m ∧ Nat.Prime n := by
+  have : 4 < 5 ∧ 5 < 7 ∧ 7 < 10 ∧ Nat.Prime 5 ∧ Nat.Prime 7 := by norm_num
+  duper [*]
+
+example {x y : ℝ} : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬y ≤ x := by
+  rintro ⟨h₀, h₁⟩
+  use h₀
+  exact fun h' ↦ h₁ (le_antisymm h₀ h')
+
+example {x y : ℝ} : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬y ≤ x := by
+  duper [le_antisymm]
+
+example {x y : ℝ} (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by
+  constructor
+  · contrapose!
+    rintro rfl
+    rfl
+  contrapose!
+  exact le_antisymm h
+
+example {x y : ℝ} (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by
+  duper [*, le_antisymm]
+
+example {x y : ℝ} : x ≤ y ∧ ¬y ≤ x ↔ x ≤ y ∧ x ≠ y := by
+  constructor
+  · rintro ⟨h0, h1⟩
+    constructor
+    · exact h0
+    intro h2
+    apply h1
+    rw [h2]
+  rintro ⟨h0, h1⟩
+  constructor
+  · exact h0
+  intro h2
+  apply h1
+  apply le_antisymm h0 h2
+
+example {x y : ℝ} : x ≤ y ∧ ¬y ≤ x ↔ x ≤ y ∧ x ≠ y := by
+  duper [le_antisymm]
+
+theorem aux {x y : ℝ} (h : x ^ 2 + y ^ 2 = 0) : x = 0 :=
+  have h' : x ^ 2 = 0 := by linarith [pow_two_nonneg x, pow_two_nonneg y]
+  pow_eq_zero h'
+
+example (x y : ℝ) : x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0 := by
+  constructor
+  · intro h
+    constructor
+    · exact aux h
+    rw [add_comm] at h
+    exact aux h
+  rintro ⟨rfl, rfl⟩
+  norm_num
+
+example (x y : ℝ) : x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0 := by
+  have : (0 : ℝ) ^ 2 = 0 := by norm_num
+  duper [*, aux, add_comm, add_zero]
+
+section
+
+-- Not good for Duper
+example (x : ℝ) : |x + 3| < 5 → -8 < x ∧ x < 2 := by
+  rw [abs_lt]
+  intro h
+  constructor <;> linarith
+
+example : 3 ∣ Nat.gcd 6 15 := by
+  rw [Nat.dvd_gcd_iff]
+  constructor <;> norm_num
+
+-- Interesting: this uses `decide` at the end
+example : 3 ∣ Nat.gcd 6 15 := by
+  duper [Nat.dvd_gcd_iff] {portfolioInstance := 7}
+
+end
+
+theorem not_monotone_iff {f : ℝ → ℝ} : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := by
+  rw [Monotone]
+  push_neg
+  rfl
+
+example {f : ℝ → ℝ} : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := by
+  duper [Monotone, not_le]
+
+example : ¬Monotone fun x : ℝ ↦ -x := by
+  rw [not_monotone_iff]
+  use 0, 1
+  norm_num
+
+example : ¬Monotone fun x : ℝ ↦ -x := by
+  duper [Monotone, not_lt, le_of_lt, neg_le_neg_iff, zero_lt_one]
+
+section
+variable {α : Type*} [PartialOrder α]
+variable (a b : α)
+
+example : a < b ↔ a ≤ b ∧ a ≠ b := by
+  rw [lt_iff_le_not_le]
+  constructor
+  · rintro ⟨h0, h1⟩
+    constructor
+    · exact h0
+    intro h2
+    apply h1
+    rw [h2]
+  rintro ⟨h0, h1⟩
+  constructor
+  · exact h0
+  intro h2
+  apply h1
+  apply le_antisymm h0 h2
+
+example : a < b ↔ a ≤ b ∧ a ≠ b := by
+  duper [lt_iff_le_not_le, le_antisymm]
+
+end
+
+section
+variable {α : Type*} [Preorder α]
+variable (a b c : α)
+
+example : ¬a < a := by
+  duper [lt_iff_le_not_le]
+
+example : a < b → b < c → a < c := by
+  duper [lt_iff_le_not_le, le_trans]
+
+end
diff --git a/DuperOnMathlib/DuperOnMathlib/MIL/C03_Logic/S05_Disjunction.lean b/DuperOnMathlib/DuperOnMathlib/MIL/C03_Logic/S05_Disjunction.lean
new file mode 100644
index 0000000..d058f6f
--- /dev/null
+++ b/DuperOnMathlib/DuperOnMathlib/MIL/C03_Logic/S05_Disjunction.lean
@@ -0,0 +1,190 @@
+import Mathlib.Data.Real.Basic
+import Duper.Tactic
+
+namespace C03S05
+
+section
+
+variable {x y : ℝ}
+
+example (h : y > x ^ 2) : y > 0 ∨ y < -1 := by
+  left
+  linarith [pow_two_nonneg x]
+
+example (h : y > x ^ 2) : y > 0 ∨ y < -1 := by
+  duper [pow_two_nonneg, h, lt_of_le_of_lt]
+
+example (h : -y > x ^ 2 + 1) : y > 0 ∨ y < -1 := by
+  right
+  linarith [pow_two_nonneg x]
+
+example (h : y > 0) : y > 0 ∨ y < -1 := by
+  duper [h]
+
+example (h : y < -1) : y > 0 ∨ y < -1 := by
+  duper [h]
+
+example : x < |y| → x < y ∨ x < -y := by
+  rcases le_or_gt 0 y with h | h
+  · rw [abs_of_nonneg h]
+    intro h; left; exact h
+  . rw [abs_of_neg h]
+    intro h; right; exact h
+
+example : x < |y| → x < y ∨ x < -y := by
+  duper [le_or_gt, abs_of_nonneg, abs_of_neg]
+
+namespace MyAbs
+
+theorem le_abs_self (x : ℝ) : x ≤ |x| := by
+  rcases le_or_gt 0 x with h | h
+  · rw [abs_of_nonneg h]
+  . rw [abs_of_neg h]
+    linarith
+
+example (x : ℝ) : x ≤ |x| := by
+  duper [le_or_gt, abs_of_nonneg, abs_of_neg, lt_trans, neg_lt_neg_iff, neg_zero, le_refl, le_of_lt]
+
+theorem neg_le_abs_self (x : ℝ) : -x ≤ |x| := by
+  rcases le_or_gt 0 x with h | h
+  · rw [abs_of_nonneg h]
+    linarith
+  . rw [abs_of_neg h]
+
+example (x : ℝ) : -x ≤ |x| := by
+  duper [le_or_gt, abs_of_nonneg, abs_of_neg, le_trans, neg_le_neg_iff, neg_zero, le_refl]
+
+theorem abs_add (x y : ℝ) : |x + y| ≤ |x| + |y| := by
+  rcases le_or_gt 0 (x + y) with h | h
+  · rw [abs_of_nonneg h]
+    linarith [le_abs_self x, le_abs_self y]
+  . rw [abs_of_neg h]
+    linarith [neg_le_abs_self x, neg_le_abs_self y]
+
+example (x y : ℝ) : |x + y| ≤ |x| + |y| := by
+  rcases le_or_gt 0 (x + y) with h | h
+  · duper [abs_of_nonneg h, le_abs_self, add_le_add, le_trans]
+  . duper [abs_of_neg h, neg_le_abs_self, add_le_add, neg_add]
+
+-- Too much for duper.
+-- example (x y : ℝ) : |x + y| ≤ |x| + |y| := by
+--   duper [le_or_gt 0 (x + y), abs_of_nonneg, le_abs_self, neg_le_abs_self, le_trans, abs_of_neg, add_le_add, neg_add]
+
+theorem lt_abs : x < |y| ↔ x < y ∨ x < -y := by
+  rcases le_or_gt 0 y with h | h
+  · rw [abs_of_nonneg h]
+    constructor
+    · intro h'
+      left
+      exact h'
+    . intro h'
+      rcases h' with h' | h'
+      · exact h'
+      . linarith
+  rw [abs_of_neg h]
+  constructor
+  · intro h'
+    right
+    exact h'
+  . intro h'
+    rcases h' with h' | h'
+    · linarith
+    . exact h'
+
+example : x < |y| ↔ x < y ∨ x < -y := by
+  have : ∀ y : ℝ, y < 0 → y < -y := by intros; linarith
+  have : ∀ y : ℝ, 0 ≤ y → -y ≤ y := by intros; linarith
+  duper [*, le_or_gt 0 y, abs_of_neg, abs_of_nonneg, lt_trans, lt_of_lt_of_le]
+
+theorem abs_lt : |x| < y ↔ -y < x ∧ x < y := by
+  rcases le_or_gt 0 x with h | h
+  · rw [abs_of_nonneg h]
+    constructor
+    · intro h'
+      constructor
+      · linarith
+      exact h'
+    . intro h'
+      rcases h' with ⟨-, h2⟩
+      exact h2
+  . rw [abs_of_neg h]
+    constructor
+    · intro h'
+      constructor
+      · linarith
+      . linarith
+    . intro h'
+      linarith
+
+example : |x| < y ↔ -y < x ∧ x < y := by
+  have : ∀ y : ℝ, y < 0 → y < -y := by intros; linarith
+  have : ∀ y : ℝ, 0 ≤ y → -y ≤ y := by intros; linarith
+  duper [*, le_or_gt 0 x, abs_of_neg, abs_of_nonneg, lt_trans, lt_of_lt_of_le, lt_of_le_of_lt, neg_lt, neg_neg]
+
+end MyAbs
+
+end
+
+example {x : ℝ} (h : x ≠ 0) : x < 0 ∨ x > 0 := by
+  rcases lt_trichotomy x 0 with xlt | xeq | xgt
+  · left
+    exact xlt
+  · contradiction
+  . right; exact xgt
+
+example {x : ℝ} (h : x ≠ 0) : x < 0 ∨ x > 0 := by
+  duper [lt_trichotomy, h]
+
+example {m n k : ℕ} (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := by
+  rcases h with ⟨a, rfl⟩ | ⟨b, rfl⟩
+  · rw [mul_assoc]
+    apply dvd_mul_right
+  . rw [mul_comm, mul_assoc]
+    apply dvd_mul_right
+
+example {m n k : ℕ} (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := by
+  duper [mul_assoc, mul_comm, dvd_mul_right, h, dvd_def]
+
+example {z : ℝ} (h : ∃ x y, z = x ^ 2 + y ^ 2 ∨ z = x ^ 2 + y ^ 2 + 1) : z ≥ 0 := by
+  rcases h with ⟨x, y, rfl | rfl⟩ <;> linarith [sq_nonneg x, sq_nonneg y]
+
+example {z : ℝ} (h : ∃ x y, z = x ^ 2 + y ^ 2 ∨ z = x ^ 2 + y ^ 2 + 1) : z ≥ 0 := by
+  duper [sq_nonneg, h, add_le_add, le_trans, zero_le_one, zero_add]
+
+example {x : ℝ} (h : x ^ 2 = 1) : x = 1 ∨ x = -1 := by
+  have h' : x ^ 2 - 1 = 0 := by rw [h, sub_self]
+  have h'' : (x + 1) * (x - 1) = 0 := by
+    rw [← h']
+    ring
+  rcases eq_zero_or_eq_zero_of_mul_eq_zero h'' with h1 | h1
+  · right
+    exact eq_neg_iff_add_eq_zero.mpr h1
+  . left
+    exact eq_of_sub_eq_zero h1
+
+-- Nice!
+example {x : ℝ} (h : x ^ 2 = 1) : x = 1 ∨ x = -1 := by
+  have h' : x ^ 2 - 1 = (x + 1) * (x - 1) := by ring
+  duper [h, h', sub_self, eq_zero_or_eq_zero_of_mul_eq_zero, eq_neg_iff_add_eq_zero, eq_of_sub_eq_zero]
+
+example {x y : ℝ} (h : x ^ 2 = y ^ 2) : x = y ∨ x = -y := by
+  have h' : x ^ 2 - y ^ 2 = 0 := by rw [h, sub_self]
+  have h'' : (x + y) * (x - y) = 0 := by
+    rw [← h']
+    ring
+  rcases eq_zero_or_eq_zero_of_mul_eq_zero h'' with h1 | h1
+  · right
+    exact eq_neg_iff_add_eq_zero.mpr h1
+  . left
+    exact eq_of_sub_eq_zero h1
+
+-- Nice!
+example {x y : ℝ} (h : x ^ 2 = y ^ 2) : x = y ∨ x = -y := by
+  have h' : x ^ 2 - y ^ 2 = (x + y) * (x - y) := by ring
+  duper [h, h', sub_self, eq_zero_or_eq_zero_of_mul_eq_zero, eq_neg_iff_add_eq_zero, eq_of_sub_eq_zero]
+
+example (P : Prop) : ¬¬P → P := by
+  duper
+
+example (P Q : Prop) : P → Q ↔ ¬P ∨ Q := by
+  duper
diff --git a/DuperOnMathlib/DuperOnMathlib/MIL/C03_Logic/S06_Sequences_and_Convergence.lean b/DuperOnMathlib/DuperOnMathlib/MIL/C03_Logic/S06_Sequences_and_Convergence.lean
new file mode 100644
index 0000000..67ad5d3
--- /dev/null
+++ b/DuperOnMathlib/DuperOnMathlib/MIL/C03_Logic/S06_Sequences_and_Convergence.lean
@@ -0,0 +1,169 @@
+import Mathlib.Data.Real.Basic
+import Duper.Tactic
+
+namespace C03S06
+
+def ConvergesTo (s : ℕ → ℝ) (a : ℝ) :=
+  ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε
+
+example : (fun x y : ℝ ↦ (x + y) ^ 2) = fun x y : ℝ ↦ x ^ 2 + 2 * x * y + y ^ 2 := by
+  ext
+  ring
+
+example (a b : ℝ) : |a| = |a - b + b| := by
+  congr
+  ring
+
+example {a : ℝ} (h : 1 < a) : a < a * a := by
+  convert (mul_lt_mul_right _).2 h
+  · rw [one_mul]
+  exact lt_trans zero_lt_one h
+
+example {a : ℝ} (h : 1 < a) : a < a * a := by
+  duper [mul_lt_mul_right, h, one_mul, lt_trans, zero_lt_one]
+
+theorem convergesTo_const (a : ℝ) : ConvergesTo (fun x : ℕ ↦ a) a := by
+  intro ε εpos
+  use 0
+  intro n nge
+  rw [sub_self, abs_zero]
+  apply εpos
+
+example (a : ℝ) : ConvergesTo (fun x : ℕ ↦ a) a := by
+  duper [ConvergesTo, sub_self, abs_zero]
+
+theorem convergesTo_add {s t : ℕ → ℝ} {a b : ℝ}
+      (cs : ConvergesTo s a) (ct : ConvergesTo t b) :
+    ConvergesTo (fun n ↦ s n + t n) (a + b) := by
+  intro ε εpos
+  dsimp
+  have ε2pos : 0 < ε / 2 := by linarith
+  rcases cs (ε / 2) ε2pos with ⟨Ns, hs⟩
+  rcases ct (ε / 2) ε2pos with ⟨Nt, ht⟩
+  use max Ns Nt
+  intro n hn
+  have ngeNs : n ≥ Ns := le_of_max_le_left hn
+  have ngeNt : n ≥ Nt := le_of_max_le_right hn
+  calc
+    |s n + t n - (a + b)| = |s n - a + (t n - b)| := by
+      congr
+      ring
+    _ ≤ |s n - a| + |t n - b| := (abs_add _ _)
+    _ < ε / 2 + ε / 2 := (add_lt_add (hs n ngeNs) (ht n ngeNt))
+    _ = ε := by norm_num
+
+example {s t : ℕ → ℝ} {a b : ℝ}
+      (cs : ConvergesTo s a) (ct : ConvergesTo t b) :
+    ConvergesTo (fun n ↦ s n + t n) (a + b) := by
+  intro ε εpos
+  dsimp
+  have ε2pos : 0 < ε / 2 := by linarith
+  rcases cs (ε / 2) ε2pos with ⟨Ns, hs⟩
+  rcases ct (ε / 2) ε2pos with ⟨Nt, ht⟩
+  use max Ns Nt
+  intro n hn
+  have ngeNs : n ≥ Ns := le_of_max_le_left hn
+  have ngeNt : n ≥ Nt := le_of_max_le_right hn
+  calc
+    |s n + t n - (a + b)| = |s n - a + (t n - b)| := by
+      congr
+      ring
+    _ ≤ |s n - a| + |t n - b| := (abs_add _ _)
+    _ < ε / 2 + ε / 2 := (add_lt_add (hs n ngeNs) (ht n ngeNt))
+    _ = ε := by norm_num
+
+
+theorem convergesTo_mul_const {s : ℕ → ℝ} {a : ℝ} (c : ℝ) (cs : ConvergesTo s a) :
+    ConvergesTo (fun n ↦ c * s n) (c * a) := by
+  by_cases h : c = 0
+  · convert convergesTo_const 0
+    · rw [h]
+      ring
+    rw [h]
+    ring
+  have acpos : 0 < |c| := abs_pos.mpr h
+  intro ε εpos
+  dsimp
+  have εcpos : 0 < ε / |c| := by apply div_pos εpos acpos
+  rcases cs (ε / |c|) εcpos with ⟨Ns, hs⟩
+  use Ns
+  intro n ngt
+  calc
+    |c * s n - c * a| = |c| * |s n - a| := by rw [← abs_mul, mul_sub]
+    _ < |c| * (ε / |c|) := (mul_lt_mul_of_pos_left (hs n ngt) acpos)
+    _ = ε := mul_div_cancel' _ (ne_of_lt acpos).symm
+
+theorem exists_abs_le_of_convergesTo {s : ℕ → ℝ} {a : ℝ} (cs : ConvergesTo s a) :
+    ∃ N b, ∀ n, N ≤ n → |s n| < b := by
+  rcases cs 1 zero_lt_one with ⟨N, h⟩
+  use N, |a| + 1
+  intro n ngt
+  calc
+    |s n| = |s n - a + a| := by
+      congr
+      abel
+    _ ≤ |s n - a| + |a| := (abs_add _ _)
+    _ < |a| + 1 := by linarith [h n ngt]
+
+theorem aux {s t : ℕ → ℝ} {a : ℝ} (cs : ConvergesTo s a) (ct : ConvergesTo t 0) :
+    ConvergesTo (fun n ↦ s n * t n) 0 := by
+  intro ε εpos
+  dsimp
+  rcases exists_abs_le_of_convergesTo cs with ⟨N₀, B, h₀⟩
+  have Bpos : 0 < B := lt_of_le_of_lt (abs_nonneg _) (h₀ N₀ (le_refl _))
+  have pos₀ : ε / B > 0 := div_pos εpos Bpos
+  rcases ct _ pos₀ with ⟨N₁, h₁⟩
+  use max N₀ N₁
+  intro n ngt
+  have ngeN₀ : n ≥ N₀ := le_of_max_le_left ngt
+  have ngeN₁ : n ≥ N₁ := le_of_max_le_right ngt
+  calc
+    |s n * t n - 0| = |s n| * |t n - 0| := by rw [sub_zero, abs_mul, sub_zero]
+    _ < B * (ε / B) := (mul_lt_mul'' (h₀ n ngeN₀) (h₁ n ngeN₁) (abs_nonneg _) (abs_nonneg _))
+    _ = ε := mul_div_cancel' _ (ne_of_lt Bpos).symm
+
+theorem convergesTo_mul {s t : ℕ → ℝ} {a b : ℝ}
+      (cs : ConvergesTo s a) (ct : ConvergesTo t b) :
+    ConvergesTo (fun n ↦ s n * t n) (a * b) := by
+  have h₁ : ConvergesTo (fun n ↦ s n * (t n + -b)) 0 := by
+    apply aux cs
+    convert convergesTo_add ct (convergesTo_const (-b))
+    ring
+  have := convergesTo_add h₁ (convergesTo_mul_const b cs)
+  convert convergesTo_add h₁ (convergesTo_mul_const b cs) using 1
+  · ext; ring
+  ring
+
+theorem convergesTo_unique {s : ℕ → ℝ} {a b : ℝ}
+      (sa : ConvergesTo s a) (sb : ConvergesTo s b) :
+    a = b := by
+  by_contra abne
+  have : |a - b| > 0 := by
+    apply lt_of_le_of_ne
+    · apply abs_nonneg
+    intro h''
+    apply abne
+    apply eq_of_abs_sub_eq_zero h''.symm
+  let ε := |a - b| / 2
+  have εpos : ε > 0 := by
+    change |a - b| / 2 > 0
+    linarith
+  rcases sa ε εpos with ⟨Na, hNa⟩
+  rcases sb ε εpos with ⟨Nb, hNb⟩
+  let N := max Na Nb
+  have absa : |s N - a| < ε := by
+    apply hNa
+    apply le_max_left
+  have absb : |s N - b| < ε := by
+    apply hNb
+    apply le_max_right
+  have : |a - b| < |a - b|
+  calc
+    |a - b| = |(-(s N - a)) + (s N - b)| := by
+      congr
+      ring
+    _ ≤ |(-(s N - a))| + |s N - b| := (abs_add _ _)
+    _ = |s N - a| + |s N - b| := by rw [abs_neg]
+    _ < ε + ε := (add_lt_add absa absb)
+    _ = |a - b| := by norm_num
+  exact lt_irrefl _ this