Strengthening inequality given neq hypotheses?

Stream: new members

[Alex Peattie]

If I have a hypothesis that, for example:

h: 0 < x

and I have hypotheses that $x \neq 1$ and $x \neq 2$:

h1: x ≠ 1
h2: x ≠ 2

is there a tactic that can help me produce a proof that $2 < x$ automagically? I thought that linarith might do it but it doesn't seem to:

have : x < 2, linarith, -- doesn't work

I can do it manually by repeatedly applying lt_of_le_of_ne for example, but I thought there might be a more Lean-ish way of doing it. Here's the #xy of what I'm actually proving:

import tactic

lemma sign_neg_cube { a : ℤ } (h_a_nz: a ≠ 0): 0 < a^3 ↔ 0 < a := sorry

theorem cube_root_two_non_integral' { x : ℤ } : x^3 = 2 → false :=
begin
  assume h,
  have hx_neqz : ¬x = 0 := begin
    by_contra hc,
    rw hc at h, ring_exp at h, cc,
  end,
  have hx_pos : 0 < x := begin
    by_contra hc,
    have := (not_iff_not_of_iff (sign_neg_cube hx_neqz)).2 hc,
    linarith,
  end,
  have hx_neq1 : ¬x = 1 := by { by_contra hc, simp * at *, cc },
  have hx_neq2 : ¬x = 2 := by { by_contra hc, rw hc at h, ring_exp at h, cc },

  -- these are the lines I'd like to get rid of
  have : 1 < x, exact lt_of_le_of_ne hx_pos (ne.symm hx_neq1),
  have : 2 < x, exact lt_of_le_of_ne this (ne.symm hx_neq2),

  have : x < 3 := begin
    by_contra hc, simp at hc,
    have := pow_lt_pow_of_lt_left this dec_trivial (by dec_trivial : 0 < 3),
    norm_num at this, linarith,
  end,
  linarith,
end

[Kenny Lau]

import tactic

theorem foo {x : ℤ} (h : 0 < x) (h1 : x ≠ 1) (h2 : x ≠ 2) : 2 < x := by omega

[Alex Peattie]

Amazing, thank you!