cmp✝ : ?m.2531 → ?m.2531 → Ordering
inst✝¹ : TransCmp cmp✝
x✝ : Sort ?u.2529
cmp : x✝ → x✝ → Ordering
inst✝ : TransCmp cmp
x y z : x✝
h₁ : cmp y x = Ordering.lt
h₂ : cmp z y = Ordering.lt
⊢ cmp z x = Ordering.lt
cmp✝ : ?m.2531 → ?m.2531 → Ordering
inst✝¹ : TransCmp cmp✝
x✝ : Sort ?u.2529
cmp : x✝ → x✝ → Ordering
inst✝ : TransCmp cmp
x y z : x✝
h₁ : cmp x y = Ordering.gt
h₂ : cmp y z = Ordering.gt
⊢ cmp x z = Ordering.gt
rw [cmp_eq_gt] at h₁ h₂ ⊢
no goals
cmp✝ : ?m.2531 → ?m.2531 → Ordering
inst✝¹ : TransCmp cmp✝
x✝ : Sort ?u.2529
cmp : x✝ → x✝ → Ordering
inst✝ : TransCmp cmp
x y z : x✝
h₁ : cmp y x = Ordering.lt
h₂ : cmp z y = Ordering.lt
⊢ cmp z x = Ordering.lt
exact lt_trans h₂ h₁