## Stream: new members

### Topic: trichotomy of naturals

#### Bhavik Mehta (Oct 27 2019 at 02:50):

I have the hypothesis ¬a = 2, where a : ℕ, and I'd like to reduce this to a <= 1 and a >= 3, is there something in the standard libs to help me?

#### Mario Carneiro (Oct 27 2019 at 03:11):

example {n : ℕ} (h : n ≠ 2) : n ≤ 1 ∨ 3 ≤ n :=
begin
cases ne_iff_lt_or_gt.1 h with h' h',
exact or.inl (nat.le_of_lt_succ h'),
exact or.inr (nat.succ_le_of_lt h'),
end


#### Kenny Lau (Oct 27 2019 at 03:14):

import tactic.omega

example {n : ℕ} (h : n ≠ 2) : n ≤ 1 ∨ 3 ≤ n :=
by rw ne_iff_lt_or_gt at h; omega


#### Bhavik Mehta (Oct 27 2019 at 14:17):

Thanks both! Is there somewhere I can search for things like this?

#### Bryan Gin-ge Chen (Oct 27 2019 at 14:33):

This doc on naming conventions may be helpful, since it will help with using autocomplete in VS Code (or emacs?) to get a list of relevant suggestions.

There's also #find:

import tactic.find

-- need to have some declaration before #find starts to work
example : true := trivial

#find _ ≠ _ → _ ≤ _ ∨ _ ≥ _
-- returns nothing, probably because using < and > would be better
#find _ ≠ _ → _ < _ ∨ _ > _
-- lt_or_gt_of_ne: ∀ {α : Type u} [_inst_1 : linear_order α] {a b : α}, a ≠ b → a < b ∨ a > b


#### Kevin Buzzard (Oct 27 2019 at 14:50):

To give an example of autocomplete here -- for a general totally ordered thing (e.g. the reals) the theorem is going to be a != x iff a < x or a > x, so I write

import tactic.linarith -- mega import to make sure I get lots of mathlib in

example (a : ℕ) : a ≠ 2 ↔ a < 2 ∨ a > 2 :=
begin
exact ne_iff
end


(because I know ne_iff... is what this thing will be called, by the naming conventions) and then I move to just after the last f of iff and (in VS Code) hit esc, ctrl-space, and then if I don't get enough stuff I hit esc, ctrl-space again (I don't know why I have to do it twice sometimes). I can now see a big list of lots of theorems which have ne_iff in, and then I can use the arrow keys to scroll around and find the one I want.

Last updated: May 13 2021 at 05:21 UTC