feat(archive/imo): IMO 2020 Q2 (#4565)
Add a proof of IMO 2020 Q2 (directly following one of the official
solutions; there are many very similar approaches possible).
In support of this solution, add `geom_mean_le_arith_mean4_weighted`
to `analysis.mean_inequalities`, for both `real` and `nnreal`,
analogous to the versions for two and three numbers (and also add
`geom_mean_le_arith_mean3_weighted` for `real` as it was only present
for `nnreal`).
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Johan Commelin <johan@commelin.net>
