refactor(archive/imo) shorten imo1013_q5 using pow_unbounded_of_one_lt (#7373)
refactor(archive/imo) shorten imo1013_q5 using pow_unbounded_of_one_lt (#7373)

Replaces a usage of `one_add_mul_sub_le_pow` with the more direct `pow_unbounded_of_one_lt`.





leanprover-community/mathlib,leanprover-community/mathlib