Proving basic inequalities of natural numbers

Stream: new members

[Sebastian Zimmer]

linarith doesn't seem to be good enough to prove this basic inequality

lemma simple_order_lemma (k : ℕ) (h1 : k > 0) (h2 : ¬ k > 1) : k = 1 := begin
sorry
end

[Sebastian Zimmer]

What's the best way of proving this sort of result?

[Kenny Lau]

import data.nat.basic

lemma simple_order_lemma (k : ℕ) (h1 : k > 0) (h2 : ¬ k > 1) : k = 1 :=
(dec_trivial : ∀ k, k ≤ 1 → k > 0 → k = 1) k (le_of_not_gt h2) h1

[Kenny Lau]

lemma simple_order_lemma (k : ℕ) (h1 : k > 0) (h2 : ¬ k > 1) : k = 1 :=
begin
  have h3 := le_of_not_gt h2,
  cases h3 with h3 h3, {refl},
  cases h3, cases h1
end

[Sebastian Zimmer]

Thanks, I would have never thought of that first solution.