Fin n → 0 < n

Stream: mathlib4

[Daniel Weber]

This lemma has three copies - docs#Fin.pos, docs#Fin.size_pos and docs#Fin.size_positive. Is there any reason for that? Should we deprecate two of them? Which?

[Johan Commelin]

I think the 3rd can definitely go.

[Johan Commelin]

I would vote to keep the 1st one, since it has the shortest name

[Mario Carneiro]

note, the first two are in core and the third is in mathlib

[Kim Morrison]

Fin.size_pos deprecated in terms of Fin.pos in lean#6025.