ltTrans.idr

leLtOrEq : (x, y : Bin) -> x `Le` y -> Either (x `Lt` y) (x=y)
leLtOrEq x y xley with (x `compare` y) proof xy
  | LT = Left Refl
  | EQ = Right $ compareEqIffTo x y (sym xy)
  | GT = absurd $ xley Refl

ltTrans : (p, q, r : Bin) -> p `Lt` q -> q `Lt` r -> p `Lt` r
ltTrans p q r = 
  peanoRect 
    (\x => (s, t : Bin) -> s `Lt` t -> t `Lt` x -> s `Lt` x)
    base 
    (\x,prf,s,t,sltt,tltsx =>
      case leLtOrEq t x $ ltSuccRTo t x tltsx of
        Left tltx =>
          ltSuccRFro s x $
          ltLeIncl s x $
          prf s t sltt tltx
        Right teqx =>
          rewrite sym teqx in
          ltSuccRFro s t $
          ltLeIncl s t sltt
    )
    r p q
    where 
    base : (n, m : Bin) -> n `Lt` m -> m `Lt` 0 -> n `Lt` 0
    base  _        BinO    _    mltz = absurd mltz
    base  _       (BinP _) _    mltz = absurd mltz