%default total

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

lte3_proof: (LTE x 2) -> (Is012 x)
lte3_proof LTEZero = IsZero
lte3_proof (LTESucc LTEZero) = IsOne
lte3_proof (LTESucc (LTESucc LTEZero)) = IsTwo


main : IO ()
main = putStrLn "Correct"