Commit 2023-06-21 09:25 9dd09eb1
View on Github →feat: golf IMO 2019 q4 (#5310)
Rewrite the IMO 2019 q4 solution to make the "implicit" calc blocks (lots of lt_of_le_of_lt) explicit, then automate some proofs.
This is not a golf in the sense of decreasing the number of lines (maybe it is if you take into account the number of lines like
intros; rw [sub_nonneg]; apply pow_le_pow; norm_num; apply le_of_lt; rwa [← mem_range]
in the original). So, if desired, I can make this an additional proof rather than a replacement to the existing proof.