is less than transitive

Stream: new members

[Patrick Thomas]

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]

The lemma is true

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

By definition this is x = z → false

[Patrick Thomas]

That is where I am stuck.

[Yury G. Kudryashov]

So, you can assume hxz : x = z

[Yury G. Kudryashov]

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

[Patrick Thomas]

Ah! Thank you!