# Zulip Chat Archive

## Stream: general

### Topic: proving obvious instances pow_pos_iff

#### Amaury Hayat (Apr 07 2022 at 19:33):

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 (Apr 07 2022 at 19:35):

I think `apply_instance`

will prove it, but it is strange it asks for it.

#### Patrick Massot (Apr 07 2022 at 19:39):

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

.

#### Patrick Massot (Apr 07 2022 at 19:39):

The proof term `(pow_pos_iff h).mpr h₀`

will be probably be ok

#### Amaury Hayat (Apr 07 2022 at 19:50):

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 (Apr 07 2022 at 19:56):

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

#### Amaury Hayat (Apr 07 2022 at 20:13):

Ok thanks ;)

Last updated: Aug 03 2023 at 10:10 UTC