pow): golf a proof (#14093)

Commit

3 years ago

chore(analysis/special_functions/pow): golf a proof (#14093) * move `real.abs_rpow_of_nonneg` up; * use it to golf a line in `real.abs_rpow_le_abs_rpow`.

Author

urkud

Parents

4977fd9d

mathlib a9665571 - chore(analysis/special_functions/pow): golf a proof (#14093)

mathlib
a9665571 - chore(analysis/special_functions/pow): golf a proof (#14093)