datatype Nat {

  zero: Nat

  add1(prev: Nat): Nat

}

function add(x: Nat, y: Nat): Nat {

  return recursion (x) {

    case zero => y

    case add1(prev, almost) =>

      add1(almost.prev)

  }

}

function add_is_commutative(

  x: Nat, y: Nat,

): Equal(Nat, add(x, y), add(y, x)) {

  return induction (x) {

    motive (x) => Equal(Nat, add(x, y), add(y, x))

    case zero => add_is_commutative_on_zero(y)

    case add1(prev, almost) =>

      equal_compose(

        equal_map(almost.prev, add1),

        equal_swap(add_is_commutative_on_add1(y, prev)),

      )

  }

}

class Group extends Monoid {

  inv(x: Element): Element

  inv_left(x: Element):

    Equal(Element, mul(inv(x), x), id)

  inv_right(x: Element):

    Equal(Element, mul(x, inv(x)), id)

  div(x: Element, y: Element): Element {

    return mul(x, inv(y))

  }

}