OAI/Combinatorics/RamseyFive/Marking/AllHistoryWindowLoss.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.SharpRamseyFive.Marking.WindowHistoryline 20 - def
OAI.SharpRamseyFive.Marking.windowPosteriorline 25 - theorem
OAI.SharpRamseyFive.Marking.allHistory_window_lossline 28