nat trivialities

Stream: general

[Patrick Massot]

I'm very bad at finding nat trivialities in mathlib, and library_search does seem to want to help me today. Where can I find:

lemma nat.forall_ge_iff {n : ℕ} {P : ℕ → Prop} : (∀ m ≥ n, P m) ↔ ∀ k, P (n + k)

lemma nat.forall_gt_iff {n : ℕ} {P : ℕ → Prop} : (∀ m > n, P m) ↔ ∀ k, P (n + 1 + k)

lemma nat.strict_mono_of_succ {u : ℕ → ℕ} (h : ∀ n, u n < u (n + 1)) : strict_mono u :=

[Patrick Massot]

Note that I can prove those lemmas, but they must be there somewhere, right?

[Kevin Buzzard]

You can only do them because there's no subtraction ;-)

[Patrick Massot]

Sure, I wouldn't call them trivialities otherwise. They would be either false or hard.

[Mario Carneiro]

I don't think we make a habit of writing lemmas of this form

[Mario Carneiro]

the closest equivalent to nat.forall_ge_iff is nat.le.dest (where's the converse?)

[Patrick Massot]

Would that be a bad habit according to you?

[Mario Carneiro]

No, although I'm not sure if they would be very effective. Perhaps they might work as manual simp lemmas

[Mario Carneiro]

I would usually just use rcases le.dest h with <n,rfl> if I had a goal that I wanted to rewrite like this

[Mario Carneiro]

The last one is in mathlib in the stuff about well orders

[Mario Carneiro]

strict_mono.nat in algebra.strict_mono

[Patrick Massot]

And now library_search confesses...

[Mario Carneiro]

I was thinking of order_embedding.nat_lt in order.order_iso but that other one is a much better fit