Terminology

Stream: general

[Sebastien Gouezel]

The following lemma is missing in the library

theorem to_nat_le_to_nat_of_le {a b : ℤ} (h : a ≤ b) : to_nat a ≤ to_nat b :=
by rw to_nat_le; exact le_trans h (le_to_nat b)

Should I call it to_nat_le_to_nat_of_le, or to_nat_mono? There are several lemmas named foo_mono in the library, but for uniformity I tend to prefer to_nat_le_to_nat_of_le (and I would be happy if all mono lemmas were renamed analogously). Strong opinions on this?

[Mario Carneiro]

I would go for to_nat_le, to_nat_le_to_nat, or to_nat_mono

[Mario Carneiro]

depending on whether there are any other reasonable similar theorems

[Mario Carneiro]

I'm not a fan of names that are considerably longer than needed for disambiguation

[Sebastien Gouezel]

OK, let's go for to_nat_le_to_nat (I don't like to_nat_mono because the natural thing to do is to start with to_nat_le and ask for autocompletion, which will fail).

[Mario Carneiro]

If it is a problem we can also have aliases, although we don't use them too often