## Stream: general

### Topic: linarith and ordinal file

#### Sebastien Gouezel (Jul 19 2020 at 13:49):

I have tried to use linarith in the file set_theory/ordinal.lean, but it doesn't work. The minimal example is as follows. Import tactic.linarith at the top of the file. In the middle of the file (Line 996), there is

theorem zero_lt_one : (0 : ordinal) < 1 :=
lt_iff_le_and_ne.2 ⟨zero_le _, ne.symm $ordinal.one_ne_zero⟩  Now, try pasting a linarith lemma before this lemma. It works. After the lemma, it fails. lemma works {a b : ℕ} (hab : a ≤ b) (h : b < a) : false := begin linarith, end theorem zero_lt_one : (0 : ordinal) < 1 := lt_iff_le_and_ne.2 ⟨zero_le _, ne.symm$ ordinal.one_ne_zero⟩

lemma fails {a b : ℕ} (hab : a ≤ b) (h : b < a) : false :=
begin
linarith,
end


So I guess linarith gets confused in some way by the ordinal lemma zero_lt_one.

(deleted)

#3455

#### Sebastien Gouezel (Jul 19 2020 at 15:09):

Thanks!

Last updated: May 11 2021 at 21:10 UTC