sub_lt_self_iff

Stream: new members

[Liam O'Connor]

I'm trying to use the theorem sub_lt_self from algebra.ordered_group
https://leanprover-community.github.io/mathlib_docs/algebra/ordered_group.html#sub_lt_self
Yet lean can't seem to find it. I imported algebra.ordered_group. What am I doing wrong?

[Mario Carneiro]

Do you have an old version of mathlib? If you ctrl-click on import algebra.ordered_group, can you find sub_lt_self in the file?

[Liam O'Connor]

Yes, I can see it there

[Kevin Buzzard]

Maybe you can try minimising and post a #mwe