Concise way of proving contradiction in linear inequalities

Stream: new members

[Andrea Delmastro]

Hello, I am looking for a concise way of proving the following contradiction:

example (x : string) (a : ℕ) (f : string → ℕ) (h₁ : a ≤ f x) (h₂ : f x < a) : false :=
begin
  sorry
end

Is there a simple way (maybe a tactic?) that doesn't bother my code with this technical lemma?

[Yaël Dillies]

exact h₁.not_lt h₂

[Yaël Dillies]

linarith will also do it, but that's a bit overpowered.

[Arthur Paulino]

Does library_search help here?

[Kevin Buzzard]

And then the begin/end (which switches from term mode to tactic mode) cancels with the exact (which switches from tactic mode into term mode)

[Andrea Delmastro]

Oops! It was way easier than I tought. Thank you all

[Arthur Paulino]

@Andrea Delmastro library_search does help:

example (x : string) (a : ℕ) (f : string → ℕ) (h₁ : a ≤ f x) (h₂ : f x < a) : false :=
  by library_search -- exact nat.lt_le_antisymm h₂ h₁