Typeclass for 0 < n?

Stream: Is there code for X?

[Ashley Blacquiere]

Is there a Lean 3 typeclass for something like 0 < n? Similar to ne_zero?

[Ruben Van de Velde]

(misread)

[Riccardo Brasca]

NeZero is rather recent, so I don't think we have something like that.

[Eric Rodriguez]

There's docs#Filter.NeBot, but I think that's the only ordered one, and I guess that zero isn't your bot anyways

[Martin Dvořák]

Why do we create typeclasses for this kind of stuff?

[Scott Morrison]

We mostly shouldn't. Typeclass search is not designed for proving. :-)

[Eric Rodriguez]

NeZero was created for flt-regular originally because carrying round all this sort of hypotheses explicitly was very annoying, and oftentimes they are easy to figure out from context (so in our case we needed that (n : R) was not zero, when n is a nat - but often we worked over Q, char zero, so this can just come from n ≠ 0, and often that comes from being explicitly succ)

[Eric Rodriguez]

ne_bot was created as that's what a lot of theorems of filters are done in that generality, and often it is part of the definition, but mathlib felt it was nice to not require this everywhere

[Ashley Blacquiere]

Hm. My need stems from an older project that I'm currently porting up to Lean 3.5 from 3.3 in preparation to move to Lean 4. The project uses [fact (0 < n)] in some definitions, which I gather is probably not ideal (and seems to be causing some problems anyway), so I'm looking for an alternative. Any suggestions?

[Ruben Van de Velde]

If you're taking about natural numbers, ne_zero/NeZero is equivalent

[Kyle Miller]

(If anyone is motivated to experiment, a potential alternative for typeclasses is having a (hn : 0 < n := by assumption) argument. Then you can either pass it in directly or set it indirectly with a have.)