propext in sub_ne_zero_of_lt

Stream: new members

[RustyYato]

I was fiddling around with UInt8 and noticed that UInt8.land (and all other bitwise ops) depend on propext. Which I found odd. So I traced it back to sub_ne_zero_of_lt, which uses simp. Here simp is eagerly using propext for no reason. Would it be fine to switch it to a more explicit proof? (The whole extent of the change is by simp -> by intro; contradiction). I can put up a PR if this is OK :smile:

[RustyYato]

For reference, here's the change in my fork: https://github.com/leanprover/lean4/compare/master...RustyYato:lean4:sub_ne_zero_of_lt

[Patrick Massot]

This PR would probably be closed without much discussion. The core team has no available time for contributions whose only purpose is to remove the use of classical logic.

[Patrick Massot]

You can read about this in lean4#2414

[RustyYato]

I see, ok thanks for letting me know!