naming help

Stream: Is there code for X?

[Scott Morrison]

From a PR: what is this lemma meant to be named?

lemma ??? {a b n : ℕ} (h : 2 * n + 1 ≤ a + b) : n + 1 ≤ a ∨ n + 1 ≤ b :=

[Yaël Dillies]

two_pigeonhole_principle? two_pigeonhole_principle_nat?

[Scott Morrison]

nat.succ_le_or_succ_le?

[Yaël Dillies]

If you wrote it as

lemma ??? {a b n : α} (h : 2 * n < a + b) : n < a ∨ n < b :=

then it would be more general.

[Scott Morrison]

Isn't that definitionally equal? :-)

[Yaël Dillies]

Of course! But your lemma above is only true for succ_orders.

[Yaël Dillies]

lt_or_lt_of_two_mul_lt_add?

[Mario Carneiro]

if you wrote it as

lemma ??? {a b m n : α} (h : m + n < a + b) : m < a ∨ n < b :=

it would be even more general

[Yaël Dillies]

Damn! What about lt_or_lt_of_add_lt_add?

[Eric Rodriguez]

I feel like there was another naming help topic, but I can't find it; what do people think this lemma should be named?

[Yury G. Kudryashov]

exists_order_of_eq_pow_padic_val_nat_exponent? Or is it too long?

[Eric Rodriguez]

feels kinda long but on the other hand it does describe the lemma perfectly, so maybe i'll go with that, thanks!

[Eric Rodriguez]

What do you think of nat.prime.exists_order_of_eq_pow_padic_val_nat_exponent? Same length in practice + allows dot notation

[Yury G. Kudryashov]

I don't use this part of the library. Note: with alias, you can have both.