%default total


-- first solution

data Is012 : (x: Nat) -> Type where
  IsZero : Is012 Z
  IsOne : Is012 (S Z)
  IsTwo : Is012 (S (S Z))

lt3_proof: (LT x 3) -> (Is012 x)
lt3_proof (LTESucc LTEZero) = IsZero
lt3_proof (LTESucc (LTESucc LTEZero)) = IsOne
lt3_proof (LTESucc (LTESucc (LTESucc LTEZero))) = IsTwo


-- second solution

lt3_proof_2: (LT x 3) -> ( (g : Type) -> ( ((x = 0) -> g) -> ((x = 1) -> g) -> ((x = 2) -> g) -> g) )
lt3_proof_2 (LTESucc LTEZero) = \t => \f0 => \f1 => \f2 => f0 Refl
lt3_proof_2  (LTESucc (LTESucc LTEZero)) = \t => \f0 => \f1 => \f2 => f1 Refl
lt3_proof_2  (LTESucc (LTESucc (LTESucc LTEZero))) = \t => \f0 => \f1 => \f2 => f2 Refl


main : IO ()
main = putStrLn "Correct"