import Erdos870.Filler

namespace Erdos870

/-- Formal version of the negation of Erdős Problem #870 for the at-most-k
representation function. -/
theorem main_theorem : Erdos870Target := by
  intro k hk C hC
  by_cases hk3 : k = 3
  · subst hk3
    exact k3_from_clustered C hC
  · have hk_gt3 : 3 < k := lt_of_le_of_ne hk (Ne.symm hk3)
    have hk4 : 4 ≤ k := Nat.succ_le_of_lt hk_gt3
    rcases larsen_larsen_order2_input with ⟨W, _⟩
    exact kge4_from_order2 W k hk4 C hC

#print axioms main_theorem

end Erdos870