import Data.Fin

%default total

nat_min' : Nat -> Nat -> Nat -> Nat -> Nat
nat_min' (S a) (S b) a_acc b_acc = nat_min' a b (S a_acc) (S b_acc)
nat_min' a Z a_acc b_acc = b_acc
nat_min' Z b a_acc b_acc = a_acc

nat_min : Nat -> Nat -> Nat
nat_min a b = nat_min' a b Z Z

main : IO ()
main = putStrLn $ show $ (nat_min 2 25)