unnecessary axioms

Stream: new members

[Nick Chopper]

it seems that nat.lt_of_sub_pos in mathlib can simply call nat.add_lt_of_lt_sub_left to avoid use of classical.choice

[Nick Chopper]

(deleted)

[Patrick Massot]

If you care about avoiding choice you can open a PR.

[Kevin Buzzard]

Mathlib has become a classical library for the most part

[Patrick Massot]

But he can still open a PR if he cares, right? Certainly I won't fix this because I don't care using choice, but that modification doesn't sound like it would make mathlib more difficult to use.

[Nick Chopper]

Not worry much about that... just want to follow https://arxiv.org/abs/1904.09193 with Lean (and avoid classical reasoning at this time)

[Mario Carneiro]

You can just use your own version of lt_of_sub_pos if you want it in your local proof

[Mario Carneiro]

if it has ended up deeply embedded as a result of, say, the proof that int is a ring, then you will need to PR to fix that