Transitivity puzzle

Transitivity.idr

data Trans : (a -> a -> Type) -> a -> a -> Type where
  Tri : p a b -> Trans p a b
  Trs : Trans p a b -> Trans p b c -> Trans p a c

succ_rel : Nat -> Nat -> Type
succ_rel k j = (S k = j)

succ_rel_theorem : Trans Transitivity.succ_rel a b -> LT a b
succ_rel_theorem (Tri Refl) = LTESucc lteRefl
succ_rel_theorem (Trs x y) = let
  xlt = succ_rel_theorem x
  ylt = succ_rel_theorem y
  in lteSuccLeft $ lteTransitive (LTESucc xlt) ylt

-- Is it possible to prove this without expanding the LTE 6 5 into this kind of a big case clause?
succ_rel_5_5 : Trans Transitivity.succ_rel 5 5 -> Void
succ_rel_5_5 x = let
  y = succ_rel_theorem x 
  in case y of
    (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))) impossible
    (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc _)))))) impossible

total
bab : LTE (S n) n -> Void
bab (LTESucc x) = bab x

succ_rel_5_5 : Trans Onsen.succ_rel 5 5 -> Void
succ_rel_5_5 x = bab (succ_rel_theorem x)

Even better, make it into an implementation:

Uninhabited (LTE (S n) n) where
  uninhabited (LTESucc x) = uninhabited x