## Stream: new members

### Topic: is less than transitive

#### Patrick Thomas (Oct 18 2020 at 19:05):

I seem to be stuck. Does this lemma actually hold? Am I missing an axiom? Did I define something wrong?

namespace hidden

class total_order (T : Type*) :=
(le : T → T → Prop)
(asymm : ∀ x y : T, le x y ∧ le y x → x = y)
(trans : ∀ x y z : T, le x y ∧ le y z → le x z)
(conn : ∀ x y : T, le x y ∨ le y x)

open total_order

-- s < t
def lt {T : Type*} [total_order T] (s t : T) : Prop := le s t ∧ ¬ s = t

lemma lt_trans {T : Type*} [total_order T] {x y z : T} : lt x y ∧ lt y z → lt x z :=
assume a1 : lt x y ∧ lt y z,
have s1 : le x y := and.left (and.left a1),
have s2 : ¬ x = y := and.right (and.left a1),
have s3 : le y z := and.left (and.right a1),
have s4 : ¬ y = z := and.right (and.right a1),
have s5 : le x z := trans x y z (and.intro s1 s3),
sorry

end hidden


#### Yury G. Kudryashov (Oct 18 2020 at 19:11):

The lemma is true

#### Yury G. Kudryashov (Oct 18 2020 at 19:12):

And you don't need lt y z; it suffices to have le y z

#### Yury G. Kudryashov (Oct 18 2020 at 19:12):

Once you know le x z, you need x ≠ z.

#### Yury G. Kudryashov (Oct 18 2020 at 19:12):

By definition this is x = z → false

#### Patrick Thomas (Oct 18 2020 at 19:12):

That is where I am stuck.

#### Yury G. Kudryashov (Oct 18 2020 at 19:13):

So, you can assume hxz : x = z

#### Yury G. Kudryashov (Oct 18 2020 at 19:13):

If you rewrite on this equality in s3, then you'll be able to apply asymm

#### Patrick Thomas (Oct 18 2020 at 19:14):

Ah! Thank you!

Last updated: May 08 2021 at 09:11 UTC