def f1 (n : Nat) (i : Int) :=
i + n -- works

def f2 (n : Nat) (i : Int) :=
n + i -- fails can't coerce Int to Nat

def f3 (n : Nat) (i : Int) :=
n + (n + (n + (n + i))) -- nested version of the previous issue

def f4 (n : Nat) (i : Int) :=
n + (n + (n * (n * i))) -- nested version of the previous issue with mixed operators

def f5 (n : Nat) (i : Int) :=
n + (n + (n * (i, i).1)) -- mixed operators and different structures