Commit 2023-06-17 05:05 ba8fa673

View on Github →

feat: port Archive.Imo.Imo2006Q3 (#5123)

Estimated changes

Modified Archive.lean

Created Archive/Imo/Imo2006Q3.lean

added theorem Imo2006Q3.four_pow_four_pos

added theorem Imo2006Q3.lhs_identity

added theorem Imo2006Q3.lhs_ineq

added theorem Imo2006Q3.mid_ineq

added theorem Imo2006Q3.proof₁

added theorem Imo2006Q3.proof₂

added theorem Imo2006Q3.rhs_ineq

added theorem Imo2006Q3.subst_proof₁

added theorem Imo2006Q3.subst_wlog

added theorem Imo2006Q3.zero_lt_32

added theorem imo2006_q3