proving obvious instances pow_pos_iff

Stream: general

[Amaury Hayat]

Hi !
I have question concerning pow_pos_iff: when I try to use it like this:

example (n a:ℕ)(h:n>0)(h₀: a>0): 0<a^n:=
begin
  rw pow_pos_iff h,
end

it gives a subgoal asking me to prove no_zero_divisors nat. Of course this is not very hard but it does not ask me to prove linear_ordered_comm_monoid_with_zero nat which is also an instance of pow_pos_iff. In fact in the nat framework it is the only rule that ever asked me to prove such obvious instances. Do you know if there is a logic behind it ?
Thanks a lot in advance !

[Riccardo Brasca]

I think apply_instance will prove it, but it is strange it asks for it.

[Patrick Massot]

This is an elaboration issue, Lean looks for the type class before figuring the type of a.

[Patrick Massot]

The proof term (pow_pos_iff h).mpr h₀ will be probably be ok

[Amaury Hayat]

Ok thanks a lot ! But isn't it strange then that it does not ask me to prove linear_ordered_comm_monoid_with_zero nat ? Thanks for the advice, apply (pow_pos_iff h).mpr h₀ works perfectly

[Yaël Dillies]

Bugs be buggy. And this one is probably not getting fixed because Lean 4 is just around the corner.

[Amaury Hayat]

Ok thanks ;)