-- 2а) определите тип для представления арифметических выражений
-- (с бинарными операциями)
inductive aexp : Type
| num : ℤ → aexp
| var : string → aexp
| add : aexp -> aexp -> aexp
| sub : aexp -> aexp -> aexp
| mul : aexp -> aexp -> aexp
| div : aexp -> aexp -> aexp

3a)
def sub : ℕ → ℕ → ℕ
  | 0 a := 0
  | b 0 := b
  | (b+1) (a+1) := sub b a