norm_num fails with simple inequalities using real exponents

[TFBloom]

While norm_num can e.g. prove 1 < 2^2 (all naturals) or (1:\R) < (2:\R)^2, it fails with (1:\R) < (2:\R)^(2:\R).

Similarly(?), neither norm_num nor linarith can prove (x:R), (x>0) implies (2:R)^x < (3:R)^x.

It would be very convenient if norm_num (and/or linarith?) could work with simple inequalities involving real exponents like this.

[digama0]

You can prove these by rewriting (2 : real) = \u (2 : nat) by norm_cast, then simp it to a natural exponent and use norm_num. For the (2:R)^x < (3:R)^x example, that's certainly out of scope of both norm_num and linarith, but mono might do the trick. You should probably bring this up on Zulip because some design work is needed for a suitable tactic to define the target language.

[TFBloom]

Thanks - I should have clarified that I can prove them via other ways (e.g. the second is an application of real.rpow_le_rpow), it was just that I'd like a tactic to work this out automatically. mono looks very useful, thank you. I'll bring this up on Zulip.