Commit 2023-06-17 11:54 73593909

View on Github →

feat: port Archive.Imo.Imo1981Q3 (#5185)

Estimated changes

Modified Archive.lean

Created Archive/Imo/Imo1981Q3.lean

added theorem Imo1981Q3.NatPredicate.imp_fib

added theorem Imo1981Q3.NatPredicate.m_pos

added theorem Imo1981Q3.NatPredicate.n_le_N

added theorem Imo1981Q3.NatPredicate.n_pos

added def Imo1981Q3.NatPredicate

added theorem Imo1981Q3.ProblemPredicate.eq_imp_1

added theorem Imo1981Q3.ProblemPredicate.m_le_n

added theorem Imo1981Q3.ProblemPredicate.reduction

added structure Imo1981Q3.ProblemPredicate

added theorem Imo1981Q3.k_bound

added theorem Imo1981Q3.m_n_bounds

added theorem Imo1981Q3.solution_bound

added theorem Imo1981Q3.solution_greatest

added def Imo1981Q3.specifiedSet

added theorem imo1981_q3