cases c₁:h₁
a b c : Answer
h₁ : a ≤ b
h₂ : b ≤ c
⊢ a ≤ c
case no_le
b c : Answer
h₂ : b ≤ c
h₁ : Answer.no ≤ b
c₁ : h₁ = ⋯
⊢ Answer.no ≤ c

case le_yes
a c : Answer
h₁ : a ≤ Answer.yes
h₂ : Answer.yes ≤ c
c₁ : h₁ = ⋯
⊢ a ≤ c

case refl
a c : Answer
h₁ : a ≤ a
h₂ : a ≤ c
c₁ : h₁ = ⋯
⊢ a ≤ c