OAI/Combinatorics/SharpRamsey/Marking/HighGoodHistory.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SharpLogRamsey.Selection.Windows.one_goodMiddle_countline 16 - theorem
OAI.SharpLogRamsey.Selection.Windows.high_good_history_halfline 24