import Base
import ./nat.bend as N
import ./int.bend as C

# int_filled.bend -- fills for int.bend.
#
# The representation is fixed by the claim file: Pos{n} is n and NegS{n}
# is -(1+n). Every operation below is written so that it computes on
# constructors, which is what makes the test cases and the embedding laws
# close with {==}.

# ---- helpers ------------------------------------------------------------

# -n, as an Int (the only place the two zeros have to be reconciled)
def Int.neg_nat(n: Nat) -> C.Int:
  match n:
    case 0n:
      C.Pos{0n}
    case 1n+p:
      C.NegS{p}

# a - b for Nats, as an Int
def Int.sub_nat(a: Nat, b: Nat) -> C.Int:
  match a b:
    case 0n 0n:
      C.Pos{0n}
    case 0n 1n+bp:
      C.NegS{bp}
    case 1n+ap 0n:
      C.Pos{1n+ap}
    case 1n+ap 1n+bp:
      Int.sub_nat(ap, bp)

# ---- operations ---------------------------------------------------------

def C.Int.neg(a):
  match a:
    case C.Pos{n}:
      Int.neg_nat(n)
    case C.NegS{n}:
      C.Pos{1n+n}

def C.Int.add(a, b):
  match a b:
    case C.Pos{x} C.Pos{y}:
      C.Pos{Nat.add(x, y)}
    case C.Pos{x} C.NegS{y}:
      Int.sub_nat(x, 1n+y)
    case C.NegS{x} C.Pos{y}:
      Int.sub_nat(y, 1n+x)
    case C.NegS{x} C.NegS{y}:
      C.NegS{1n+Nat.add(x, y)}

def C.Int.mul(a, b):
  match a b:
    case C.Pos{x} C.Pos{y}:
      C.Pos{Nat.mul(x, y)}
    case C.Pos{x} C.NegS{y}:
      Int.neg_nat(Nat.mul(x, 1n+y))
    case C.NegS{x} C.Pos{y}:
      Int.neg_nat(Nat.mul(1n+x, y))
    case C.NegS{x} C.NegS{y}:
      C.Pos{Nat.mul(1n+x, 1n+y)}

def C.Int.sub(a, b):
  C.Int.add(a, C.Int.neg(b))

def C.Int.abs(a):
  match a:
    case C.Pos{n}:
      n
    case C.NegS{n}:
      1n+n

def C.Int.Le(a, b):
  match a b:
    case C.Pos{x} C.Pos{y}:
      N.Nat.Le(x, y)
    case C.Pos{x} C.NegS{y}:
      Empty
    case C.NegS{x} C.Pos{y}:
      Unit
    case C.NegS{x} C.NegS{y}:
      N.Nat.Le(y, x)

# ---- test cases ---------------------------------------------------------

def C.t_add_1():
  {==}

def C.t_add_2():
  {==}

def C.t_mul_1():
  {==}

def C.t_mul_2():
  {==}

def C.t_sub_1():
  {==}

def C.t_abs_1():
  {==}

# ---- laws ---------------------------------------------------------------

def C.of_add(a, b):
  {==}

def C.of_mul(a, b):
  {==}

def C.sub_def(a, b):
  {==}

# n - n = 0
def Int.sub_nat_self(n: Nat) -> {Int.sub_nat(n, n) == C.Pos{0n} : C.Int}:
  match n:
    case 0n:
      {==}
    case 1n+p:
      Int.sub_nat_self(p)

def C.add_neg(a):
  match a:
    case C.Pos{n}:
      match n:
        case 0n:
          {==}
        case 1n+p:
          Int.sub_nat_self(p)
    case C.NegS{n}:
      Int.sub_nat_self(n)

def C.neg_neg(a):
  match a:
    case C.Pos{n}:
      match n:
        case 0n:
          {==}
        case 1n+p:
          {==}
    case C.NegS{n}:
      {==}

def C.add_zero(a):
  match a:
    case C.Pos{n}:
      %N.Nat.add_zero(n) : {C.Pos{Nat.add(n, 0n)} == C.Pos{_} : C.Int}
      {==}
    case C.NegS{n}:
      {==}

def C.add_comm(a, b):
  match a b:
    case C.Pos{x} C.Pos{y}:
      %N.Nat.add_comm(x, y) : {C.Pos{Nat.add(x, y)} == C.Pos{_} : C.Int}
      {==}
    case C.Pos{x} C.NegS{y}:
      {==}
    case C.NegS{x} C.Pos{y}:
      {==}
    case C.NegS{x} C.NegS{y}:
      %N.Nat.add_comm(x, y) : {C.NegS{1n+Nat.add(x, y)} == C.NegS{1n+_} : C.Int}
      {==}

def C.mul_one(a):
  match a:
    case C.Pos{n}:
      %N.Nat.mul_one(n) : {C.Pos{Nat.mul(n, 1n)} == C.Pos{_} : C.Int}
      {==}
    case C.NegS{n}:
      %N.Nat.mul_one(n) : {C.NegS{Nat.mul(n, 1n)} == C.NegS{_} : C.Int}
      {==}

def C.mul_zero(a):
  match a:
    case C.Pos{n}:
      %N.Nat.mul_zero(n) : {C.Pos{Nat.mul(n, 0n)} == C.Pos{_} : C.Int}
      {==}
    case C.NegS{n}:
      %Equal.sym(Nat, Nat.mul(n, 0n), 0n, N.Nat.mul_zero(n)) : {Int.neg_nat(_) == C.Pos{0n} : C.Int}
      {==}

def C.mul_comm(a, b):
  match a b:
    case C.Pos{x} C.Pos{y}:
      %N.Nat.mul_comm(x, y) : {C.Pos{Nat.mul(x, y)} == C.Pos{_} : C.Int}
      {==}
    case C.Pos{x} C.NegS{y}:
      %N.Nat.mul_comm(x, 1n+y) : {Int.neg_nat(Nat.mul(x, 1n+y)) == Int.neg_nat(_) : C.Int}
      {==}
    case C.NegS{x} C.Pos{y}:
      %N.Nat.mul_comm(1n+x, y) : {Int.neg_nat(Nat.mul(1n+x, y)) == Int.neg_nat(_) : C.Int}
      {==}
    case C.NegS{x} C.NegS{y}:
      %N.Nat.mul_comm(1n+x, 1n+y) : {C.Pos{Nat.mul(1n+x, 1n+y)} == C.Pos{_} : C.Int}
      {==}

def C.le_refl(a):
  match a:
    case C.Pos{n}:
      N.Nat.le_refl(n)
    case C.NegS{n}:
      N.Nat.le_refl(n)

def C.le_antisym(a, b, h1, h2):
  match a b:
    case C.Pos{x} C.Pos{y}:
      %N.Nat.le_antisym(x, y, h1, h2) : {C.Pos{x} == C.Pos{_} : C.Int}
      {==}
    case C.Pos{x} C.NegS{y}:
      match h1:
    case C.NegS{x} C.Pos{y}:
      match h2:
    case C.NegS{x} C.NegS{y}:
      %N.Nat.le_antisym(x, y, h2, h1) : {C.NegS{x} == C.NegS{_} : C.Int}
      {==}

def C.le_trans(a, b, c, h1, h2):
  match a b c:
    case C.Pos{x} C.Pos{y} C.Pos{z}:
      N.Nat.le_trans(x, y, z, h1, h2)
    case C.Pos{x} C.Pos{y} C.NegS{z}:
      match h2:
    case C.Pos{x} C.NegS{y} C.Pos{z}:
      match h1:
    case C.Pos{x} C.NegS{y} C.NegS{z}:
      match h1:
    case C.NegS{x} C.Pos{y} C.Pos{z}:
      Unit{}
    case C.NegS{x} C.Pos{y} C.NegS{z}:
      match h2:
    case C.NegS{x} C.NegS{y} C.Pos{z}:
      Unit{}
    case C.NegS{x} C.NegS{y} C.NegS{z}:
      N.Nat.le_trans(z, y, x, h2, h1)

def C.pos_nonneg(n):
  Unit{}

# ---- the difference view -------------------------------------------------
#
# Every Int is Int.sub_nat(p, m) for a pair of Nats, and the operations
# act on such pairs the way school arithmetic says. Proving that once
# turns the ring laws into Nat lemmas.

def Int.toP(a: C.Int) -> Nat:
  match a:
    case C.Pos{n}:
      n
    case C.NegS{n}:
      0n

def Int.toM(a: C.Int) -> Nat:
  match a:
    case C.Pos{n}:
      0n
    case C.NegS{n}:
      1n+n

def Int.sub_nat_zero(x: Nat) -> {Int.sub_nat(x, 0n) == C.Pos{x} : C.Int}:
  match x:
    case 0n:
      {==}
    case 1n+xp:
      {==}

def Int.sub_nat_zero_l(x: Nat) -> {Int.sub_nat(0n, x) == Int.neg_nat(x) : C.Int}:
  match x:
    case 0n:
      {==}
    case 1n+xp:
      {==}

def Int.split(a: C.Int) -> {Int.sub_nat(Int.toP(a), Int.toM(a)) == a : C.Int}:
  match a:
    case C.Pos{n}:
      Int.sub_nat_zero(n)
    case C.NegS{n}:
      {==}

def Int.by1(-P: C.Int -> Type, +a: C.Int, w: P(Int.sub_nat(Int.toP(a), Int.toM(a)))) -> P(a):
  %Int.split(a) : P(_)
  w

def Int.by2(-P: C.Int -> C.Int -> Type, +a: C.Int, +b: C.Int, w: P(Int.sub_nat(Int.toP(a), Int.toM(a)), Int.sub_nat(Int.toP(b), Int.toM(b)))) -> P(a, b):
  %Int.split(a) : P(_, b)
  %Int.split(b) : P(Int.sub_nat(Int.toP(a), Int.toM(a)), _)
  w

def Int.by3(-P: C.Int -> C.Int -> C.Int -> Type, +a: C.Int, +b: C.Int, +c: C.Int, w: P(Int.sub_nat(Int.toP(a), Int.toM(a)), Int.sub_nat(Int.toP(b), Int.toM(b)), Int.sub_nat(Int.toP(c), Int.toM(c)))) -> P(a, b, c):
  %Int.split(a) : P(_, b, c)
  %Int.split(b) : P(Int.sub_nat(Int.toP(a), Int.toM(a)), _, c)
  %Int.split(c) : P(Int.sub_nat(Int.toP(a), Int.toM(a)), Int.sub_nat(Int.toP(b), Int.toM(b)), _)
  w

# p + (q - n) = (p + q) - n
def Int.add_pos(+x: Nat, q: Nat, n: Nat) -> {C.Int.add(C.Pos{x}, Int.sub_nat(q, n)) == Int.sub_nat(Nat.add(x, q), n) : C.Int}:
  match q n:
    case 0n 0n:
      Equal.sym(C.Int, Int.sub_nat(Nat.add(x, 0n), 0n), C.Pos{Nat.add(x, 0n)}, Int.sub_nat_zero(Nat.add(x, 0n)))
    case 0n 1n+np:
      %N.Nat.add_zero(x) : {Int.sub_nat(_, 1n+np) == Int.sub_nat(Nat.add(x, 0n), 1n+np) : C.Int}
      {==}
    case 1n+qp 0n:
      Equal.sym(C.Int, Int.sub_nat(Nat.add(x, 1n+qp), 0n), C.Pos{Nat.add(x, 1n+qp)}, Int.sub_nat_zero(Nat.add(x, 1n+qp)))
    case 1n+qp 1n+np:
      %Equal.sym(Nat, Nat.add(x, 1n+qp), 1n+Nat.add(x, qp), N.Nat.add_succ(x, qp)) : {C.Int.add(C.Pos{x}, Int.sub_nat(qp, np)) == Int.sub_nat(_, 1n+np) : C.Int}
      Int.add_pos(x, qp, np)

# -(1+m) + (q - n) = q - (1 + m + n)
def Int.add_negs(+m: Nat, q: Nat, n: Nat) -> {C.Int.add(C.NegS{m}, Int.sub_nat(q, n)) == Int.sub_nat(q, 1n+Nat.add(m, n)) : C.Int}:
  match q n:
    case 0n 0n:
      %Equal.sym(Nat, Nat.add(m, 0n), m, N.Nat.add_zero(m)) : {C.NegS{m} == C.NegS{_} : C.Int}
      {==}
    case 0n 1n+np:
      %N.Nat.add_succ(m, np) : {C.NegS{_} == C.NegS{Nat.add(m, 1n+np)} : C.Int}
      {==}
    case 1n+qp 0n:
      %Equal.sym(Nat, Nat.add(m, 0n), m, N.Nat.add_zero(m)) : {Int.sub_nat(qp, m) == Int.sub_nat(qp, _) : C.Int}
      {==}
    case 1n+qp 1n+np:
      %Equal.sym(Nat, Nat.add(m, 1n+np), 1n+Nat.add(m, np), N.Nat.add_succ(m, np)) : {C.Int.add(C.NegS{m}, Int.sub_nat(qp, np)) == Int.sub_nat(qp, _) : C.Int}
      Int.add_negs(m, qp, np)

# (p - m) + (q - n) = (p + q) - (m + n)
def Int.add_sub(p: Nat, m: Nat, +q: Nat, +n: Nat) -> {C.Int.add(Int.sub_nat(p, m), Int.sub_nat(q, n)) == Int.sub_nat(Nat.add(p, q), Nat.add(m, n)) : C.Int}:
  match p m:
    case 0n 0n:
      Int.add_pos(0n, q, n)
    case 0n 1n+mp:
      Int.add_negs(mp, q, n)
    case 1n+pp 0n:
      Int.add_pos(1n+pp, q, n)
    case 1n+pp 1n+mp:
      Int.add_sub(pp, mp, q, n)

def Int.add_assoc.core(+p1: Nat, +m1: Nat, +p2: Nat, +m2: Nat, +p3: Nat, +m3: Nat) -> {C.Int.add(Int.sub_nat(p1, m1), C.Int.add(Int.sub_nat(p2, m2), Int.sub_nat(p3, m3))) == C.Int.add(C.Int.add(Int.sub_nat(p1, m1), Int.sub_nat(p2, m2)), Int.sub_nat(p3, m3)) : C.Int}:
  %Equal.sym(C.Int, C.Int.add(Int.sub_nat(p2, m2), Int.sub_nat(p3, m3)), Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3)), Int.add_sub(p2, m2, p3, m3)) : {C.Int.add(Int.sub_nat(p1, m1), _) == C.Int.add(C.Int.add(Int.sub_nat(p1, m1), Int.sub_nat(p2, m2)), Int.sub_nat(p3, m3)) : C.Int}
  %Equal.sym(C.Int, C.Int.add(Int.sub_nat(p1, m1), Int.sub_nat(p2, m2)), Int.sub_nat(Nat.add(p1, p2), Nat.add(m1, m2)), Int.add_sub(p1, m1, p2, m2)) : {C.Int.add(Int.sub_nat(p1, m1), Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3))) == C.Int.add(_, Int.sub_nat(p3, m3)) : C.Int}
  %Equal.sym(C.Int, C.Int.add(Int.sub_nat(p1, m1), Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3))), Int.sub_nat(Nat.add(p1, Nat.add(p2, p3)), Nat.add(m1, Nat.add(m2, m3))), Int.add_sub(p1, m1, Nat.add(p2, p3), Nat.add(m2, m3))) : {_ == C.Int.add(Int.sub_nat(Nat.add(p1, p2), Nat.add(m1, m2)), Int.sub_nat(p3, m3)) : C.Int}
  %Equal.sym(C.Int, C.Int.add(Int.sub_nat(Nat.add(p1, p2), Nat.add(m1, m2)), Int.sub_nat(p3, m3)), Int.sub_nat(Nat.add(Nat.add(p1, p2), p3), Nat.add(Nat.add(m1, m2), m3)), Int.add_sub(Nat.add(p1, p2), Nat.add(m1, m2), p3, m3)) : {Int.sub_nat(Nat.add(p1, Nat.add(p2, p3)), Nat.add(m1, Nat.add(m2, m3))) == _ : C.Int}
  %N.Nat.add_assoc(p1, p2, p3) : {Int.sub_nat(Nat.add(p1, Nat.add(p2, p3)), Nat.add(m1, Nat.add(m2, m3))) == Int.sub_nat(_, Nat.add(Nat.add(m1, m2), m3)) : C.Int}
  %N.Nat.add_assoc(m1, m2, m3) : {Int.sub_nat(Nat.add(p1, Nat.add(p2, p3)), Nat.add(m1, Nat.add(m2, m3))) == Int.sub_nat(Nat.add(p1, Nat.add(p2, p3)), _) : C.Int}
  {==}

def C.add_assoc(a, b, c):
  Int.by3(x => y => z => {C.Int.add(x, C.Int.add(y, z)) == C.Int.add(C.Int.add(x, y), z) : C.Int}, a, b, c,
    Int.add_assoc.core(Int.toP(a), Int.toM(a), Int.toP(b), Int.toM(b), Int.toP(c), Int.toM(c)))

# (k+u) - (k+v) = u - v
def Int.sub_nat_cancel(k: Nat, -u: Nat, -v: Nat) -> {Int.sub_nat(Nat.add(k, u), Nat.add(k, v)) == Int.sub_nat(u, v) : C.Int}:
  match k:
    case 0n:
      {==}
    case 1n+kp:
      Int.sub_nat_cancel(kp, u, v)

# x * (q - n) = xq - xn
def Int.mul_pos(+x: Nat, q: Nat, n: Nat) -> {C.Int.mul(C.Pos{x}, Int.sub_nat(q, n)) == Int.sub_nat(Nat.mul(x, q), Nat.mul(x, n)) : C.Int}:
  match q n:
    case 0n 0n:
      %Equal.sym(Nat, Nat.mul(x, 0n), 0n, N.Nat.mul_zero(x)) : {C.Pos{_} == Int.sub_nat(_, _) : C.Int}
      {==}
    case 0n 1n+np:
      %Equal.sym(Nat, Nat.mul(x, 0n), 0n, N.Nat.mul_zero(x)) : {Int.neg_nat(Nat.mul(x, 1n+np)) == Int.sub_nat(_, Nat.mul(x, 1n+np)) : C.Int}
      Equal.sym(C.Int, Int.sub_nat(0n, Nat.mul(x, 1n+np)), Int.neg_nat(Nat.mul(x, 1n+np)), Int.sub_nat_zero_l(Nat.mul(x, 1n+np)))
    case 1n+qp 0n:
      %Equal.sym(Nat, Nat.mul(x, 0n), 0n, N.Nat.mul_zero(x)) : {C.Pos{Nat.mul(x, 1n+qp)} == Int.sub_nat(Nat.mul(x, 1n+qp), _) : C.Int}
      Equal.sym(C.Int, Int.sub_nat(Nat.mul(x, 1n+qp), 0n), C.Pos{Nat.mul(x, 1n+qp)}, Int.sub_nat_zero(Nat.mul(x, 1n+qp)))
    case 1n+qp 1n+np:
      +qp2 = qp
      +np2 = np
      %Equal.sym(Nat, Nat.mul(x, 1n+qp2), Nat.add(x, Nat.mul(x, qp2)), N.Nat.mul_succ(x, qp2)) : {C.Int.mul(C.Pos{x}, Int.sub_nat(qp2, np2)) == Int.sub_nat(_, Nat.mul(x, 1n+np2)) : C.Int}
      %Equal.sym(Nat, Nat.mul(x, 1n+np2), Nat.add(x, Nat.mul(x, np2)), N.Nat.mul_succ(x, np2)) : {C.Int.mul(C.Pos{x}, Int.sub_nat(qp2, np2)) == Int.sub_nat(Nat.add(x, Nat.mul(x, qp2)), _) : C.Int}
      Equal.trans(C.Int, C.Int.mul(C.Pos{x}, Int.sub_nat(qp2, np2)), Int.sub_nat(Nat.mul(x, qp2), Nat.mul(x, np2)), Int.sub_nat(Nat.add(x, Nat.mul(x, qp2)), Nat.add(x, Nat.mul(x, np2))), Int.mul_pos(x, qp2, np2), Equal.sym(C.Int, Int.sub_nat(Nat.add(x, Nat.mul(x, qp2)), Nat.add(x, Nat.mul(x, np2))), Int.sub_nat(Nat.mul(x, qp2), Nat.mul(x, np2)), Int.sub_nat_cancel(x, Nat.mul(x, qp2), Nat.mul(x, np2))))

# -(1+m) * (q - n) = (1+m)n - (1+m)q
def Int.mul_negs(+m: Nat, q: Nat, n: Nat) -> {C.Int.mul(C.NegS{m}, Int.sub_nat(q, n)) == Int.sub_nat(Nat.mul(1n+m, n), Nat.mul(1n+m, q)) : C.Int}:
  match q n:
    case 0n 0n:
      %Equal.sym(Nat, Nat.mul(1n+m, 0n), 0n, N.Nat.mul_zero(1n+m)) : {Int.neg_nat(_) == Int.sub_nat(_, _) : C.Int}
      {==}
    case 0n 1n+np:
      %Equal.sym(Nat, Nat.mul(1n+m, 0n), 0n, N.Nat.mul_zero(1n+m)) : {C.Pos{Nat.mul(1n+m, 1n+np)} == Int.sub_nat(Nat.mul(1n+m, 1n+np), _) : C.Int}
      Equal.sym(C.Int, Int.sub_nat(Nat.mul(1n+m, 1n+np), 0n), C.Pos{Nat.mul(1n+m, 1n+np)}, Int.sub_nat_zero(Nat.mul(1n+m, 1n+np)))
    case 1n+qp 0n:
      %Equal.sym(Nat, Nat.mul(1n+m, 0n), 0n, N.Nat.mul_zero(1n+m)) : {Int.neg_nat(Nat.mul(1n+m, 1n+qp)) == Int.sub_nat(_, Nat.mul(1n+m, 1n+qp)) : C.Int}
      Equal.sym(C.Int, Int.sub_nat(0n, Nat.mul(1n+m, 1n+qp)), Int.neg_nat(Nat.mul(1n+m, 1n+qp)), Int.sub_nat_zero_l(Nat.mul(1n+m, 1n+qp)))
    case 1n+qp 1n+np:
      +qp2 = qp
      +np2 = np
      %Equal.sym(Nat, Nat.mul(1n+m, 1n+np2), Nat.add(1n+m, Nat.mul(1n+m, np2)), N.Nat.mul_succ(1n+m, np2)) : {C.Int.mul(C.NegS{m}, Int.sub_nat(qp2, np2)) == Int.sub_nat(_, Nat.mul(1n+m, 1n+qp2)) : C.Int}
      %Equal.sym(Nat, Nat.mul(1n+m, 1n+qp2), Nat.add(1n+m, Nat.mul(1n+m, qp2)), N.Nat.mul_succ(1n+m, qp2)) : {C.Int.mul(C.NegS{m}, Int.sub_nat(qp2, np2)) == Int.sub_nat(Nat.add(1n+m, Nat.mul(1n+m, np2)), _) : C.Int}
      Equal.trans(C.Int, C.Int.mul(C.NegS{m}, Int.sub_nat(qp2, np2)), Int.sub_nat(Nat.mul(1n+m, np2), Nat.mul(1n+m, qp2)), Int.sub_nat(Nat.add(1n+m, Nat.mul(1n+m, np2)), Nat.add(1n+m, Nat.mul(1n+m, qp2))), Int.mul_negs(m, qp2, np2), Equal.sym(C.Int, Int.sub_nat(Nat.add(1n+m, Nat.mul(1n+m, np2)), Nat.add(1n+m, Nat.mul(1n+m, qp2))), Int.sub_nat(Nat.mul(1n+m, np2), Nat.mul(1n+m, qp2)), Int.sub_nat_cancel(1n+m, Nat.mul(1n+m, np2), Nat.mul(1n+m, qp2))))

def Int.mul_add.core(a: C.Int, +p2: Nat, +m2: Nat, +p3: Nat, +m3: Nat) -> {C.Int.mul(a, C.Int.add(Int.sub_nat(p2, m2), Int.sub_nat(p3, m3))) == C.Int.add(C.Int.mul(a, Int.sub_nat(p2, m2)), C.Int.mul(a, Int.sub_nat(p3, m3))) : C.Int}:
  match a:
    case C.Pos{x}:
      +x2 = x
      %Equal.sym(C.Int, C.Int.add(Int.sub_nat(p2, m2), Int.sub_nat(p3, m3)), Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3)), Int.add_sub(p2, m2, p3, m3)) : {C.Int.mul(C.Pos{x2}, _) == C.Int.add(C.Int.mul(C.Pos{x2}, Int.sub_nat(p2, m2)), C.Int.mul(C.Pos{x2}, Int.sub_nat(p3, m3))) : C.Int}
      %Equal.sym(C.Int, C.Int.mul(C.Pos{x2}, Int.sub_nat(p2, m2)), Int.sub_nat(Nat.mul(x2, p2), Nat.mul(x2, m2)), Int.mul_pos(x2, p2, m2)) : {C.Int.mul(C.Pos{x2}, Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3))) == C.Int.add(_, C.Int.mul(C.Pos{x2}, Int.sub_nat(p3, m3))) : C.Int}
      %Equal.sym(C.Int, C.Int.mul(C.Pos{x2}, Int.sub_nat(p3, m3)), Int.sub_nat(Nat.mul(x2, p3), Nat.mul(x2, m3)), Int.mul_pos(x2, p3, m3)) : {C.Int.mul(C.Pos{x2}, Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3))) == C.Int.add(Int.sub_nat(Nat.mul(x2, p2), Nat.mul(x2, m2)), _) : C.Int}
      %Equal.sym(C.Int, C.Int.mul(C.Pos{x2}, Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3))), Int.sub_nat(Nat.mul(x2, Nat.add(p2, p3)), Nat.mul(x2, Nat.add(m2, m3))), Int.mul_pos(x2, Nat.add(p2, p3), Nat.add(m2, m3))) : {_ == C.Int.add(Int.sub_nat(Nat.mul(x2, p2), Nat.mul(x2, m2)), Int.sub_nat(Nat.mul(x2, p3), Nat.mul(x2, m3))) : C.Int}
      %Equal.sym(C.Int, C.Int.add(Int.sub_nat(Nat.mul(x2, p2), Nat.mul(x2, m2)), Int.sub_nat(Nat.mul(x2, p3), Nat.mul(x2, m3))), Int.sub_nat(Nat.add(Nat.mul(x2, p2), Nat.mul(x2, p3)), Nat.add(Nat.mul(x2, m2), Nat.mul(x2, m3))), Int.add_sub(Nat.mul(x2, p2), Nat.mul(x2, m2), Nat.mul(x2, p3), Nat.mul(x2, m3))) : {Int.sub_nat(Nat.mul(x2, Nat.add(p2, p3)), Nat.mul(x2, Nat.add(m2, m3))) == _ : C.Int}
      %N.Nat.mul_add(x2, p2, p3) : {Int.sub_nat(Nat.mul(x2, Nat.add(p2, p3)), Nat.mul(x2, Nat.add(m2, m3))) == Int.sub_nat(_, Nat.add(Nat.mul(x2, m2), Nat.mul(x2, m3))) : C.Int}
      %N.Nat.mul_add(x2, m2, m3) : {Int.sub_nat(Nat.mul(x2, Nat.add(p2, p3)), Nat.mul(x2, Nat.add(m2, m3))) == Int.sub_nat(Nat.mul(x2, Nat.add(p2, p3)), _) : C.Int}
      {==}
    case C.NegS{m}:
      +m2b = m
      %Equal.sym(C.Int, C.Int.add(Int.sub_nat(p2, m2), Int.sub_nat(p3, m3)), Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3)), Int.add_sub(p2, m2, p3, m3)) : {C.Int.mul(C.NegS{m2b}, _) == C.Int.add(C.Int.mul(C.NegS{m2b}, Int.sub_nat(p2, m2)), C.Int.mul(C.NegS{m2b}, Int.sub_nat(p3, m3))) : C.Int}
      %Equal.sym(C.Int, C.Int.mul(C.NegS{m2b}, Int.sub_nat(p2, m2)), Int.sub_nat(Nat.mul(1n+m2b, m2), Nat.mul(1n+m2b, p2)), Int.mul_negs(m2b, p2, m2)) : {C.Int.mul(C.NegS{m2b}, Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3))) == C.Int.add(_, C.Int.mul(C.NegS{m2b}, Int.sub_nat(p3, m3))) : C.Int}
      %Equal.sym(C.Int, C.Int.mul(C.NegS{m2b}, Int.sub_nat(p3, m3)), Int.sub_nat(Nat.mul(1n+m2b, m3), Nat.mul(1n+m2b, p3)), Int.mul_negs(m2b, p3, m3)) : {C.Int.mul(C.NegS{m2b}, Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3))) == C.Int.add(Int.sub_nat(Nat.mul(1n+m2b, m2), Nat.mul(1n+m2b, p2)), _) : C.Int}
      %Equal.sym(C.Int, C.Int.mul(C.NegS{m2b}, Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3))), Int.sub_nat(Nat.mul(1n+m2b, Nat.add(m2, m3)), Nat.mul(1n+m2b, Nat.add(p2, p3))), Int.mul_negs(m2b, Nat.add(p2, p3), Nat.add(m2, m3))) : {_ == C.Int.add(Int.sub_nat(Nat.mul(1n+m2b, m2), Nat.mul(1n+m2b, p2)), Int.sub_nat(Nat.mul(1n+m2b, m3), Nat.mul(1n+m2b, p3))) : C.Int}
      %Equal.sym(C.Int, C.Int.add(Int.sub_nat(Nat.mul(1n+m2b, m2), Nat.mul(1n+m2b, p2)), Int.sub_nat(Nat.mul(1n+m2b, m3), Nat.mul(1n+m2b, p3))), Int.sub_nat(Nat.add(Nat.mul(1n+m2b, m2), Nat.mul(1n+m2b, m3)), Nat.add(Nat.mul(1n+m2b, p2), Nat.mul(1n+m2b, p3))), Int.add_sub(Nat.mul(1n+m2b, m2), Nat.mul(1n+m2b, p2), Nat.mul(1n+m2b, m3), Nat.mul(1n+m2b, p3))) : {Int.sub_nat(Nat.mul(1n+m2b, Nat.add(m2, m3)), Nat.mul(1n+m2b, Nat.add(p2, p3))) == _ : C.Int}
      %N.Nat.mul_add(1n+m2b, m2, m3) : {Int.sub_nat(Nat.mul(1n+m2b, Nat.add(m2, m3)), Nat.mul(1n+m2b, Nat.add(p2, p3))) == Int.sub_nat(_, Nat.add(Nat.mul(1n+m2b, p2), Nat.mul(1n+m2b, p3))) : C.Int}
      %N.Nat.mul_add(1n+m2b, p2, p3) : {Int.sub_nat(Nat.mul(1n+m2b, Nat.add(m2, m3)), Nat.mul(1n+m2b, Nat.add(p2, p3))) == Int.sub_nat(Nat.mul(1n+m2b, Nat.add(m2, m3)), _) : C.Int}
      {==}

def C.mul_add(a, b, c):
  Int.by2(y => z => {C.Int.mul(a, C.Int.add(y, z)) == C.Int.add(C.Int.mul(a, y), C.Int.mul(a, z)) : C.Int}, b, c,
    Int.mul_add.core(a, Int.toP(b), Int.toM(b), Int.toP(c), Int.toM(c)))

# ---- the order, through the same view -----------------------------------
#
# Int.Le(p - m, q - n) is exactly Nat.Le(p + n, q + m). Both directions
# are needed: the forward one to open a hypothesis, the backward one to
# close a goal.

def Int.le_cast(-x: Nat, -y: Nat, -c: Nat, e: {x == y : Nat}, h: N.Nat.Le(x, c)) -> N.Nat.Le(y, c):
  %e : N.Nat.Le(_, c)
  h

def Int.le_cast_r(-x: Nat, -y: Nat, -c: Nat, e: {x == y : Nat}, h: N.Nat.Le(c, x)) -> N.Nat.Le(c, y):
  %e : N.Nat.Le(c, _)
  h

def Int.le_succ_zero(-k: Nat, h: N.Nat.Le(1n+k, 0n)) -> Empty:
  match h:

def Int.neg_sub(p: Nat, m: Nat) -> {C.Int.neg(Int.sub_nat(p, m)) == Int.sub_nat(m, p) : C.Int}:
  match p m:
    case 0n 0n:
      {==}
    case 0n 1n+mp:
      {==}
    case 1n+pp 0n:
      {==}
    case 1n+pp 1n+mp:
      Int.neg_sub(pp, mp)

def Int.le_pos_f(+x: Nat, q: Nat, n: Nat, h: C.Int.Le(C.Pos{x}, Int.sub_nat(q, n))) -> N.Nat.Le(Nat.add(x, n), q):
  match q n:
    case 0n 0n:
      %Equal.sym(Nat, Nat.add(x, 0n), x, N.Nat.add_zero(x)) : N.Nat.Le(_, 0n)
      h
    case 0n 1n+np:
      match h:
    case 1n+qp 0n:
      %Equal.sym(Nat, Nat.add(x, 0n), x, N.Nat.add_zero(x)) : N.Nat.Le(_, 1n+qp)
      h
    case 1n+qp 1n+np:
      %Equal.sym(Nat, Nat.add(x, 1n+np), 1n+Nat.add(x, np), N.Nat.add_succ(x, np)) : N.Nat.Le(_, 1n+qp)
      Int.le_pos_f(x, qp, np, h)

def Int.le_negs_f(+m: Nat, q: Nat, n: Nat, h: C.Int.Le(C.NegS{m}, Int.sub_nat(q, n))) -> N.Nat.Le(n, Nat.add(q, 1n+m)):
  match q n:
    case 0n 0n:
      Unit{}
    case 0n 1n+np:
      h
    case 1n+qp 0n:
      Unit{}
    case 1n+qp 1n+np:
      Int.le_negs_f(m, qp, np, h)

def Int.le_f(p: Nat, m: Nat, +q: Nat, +n: Nat, h: C.Int.Le(Int.sub_nat(p, m), Int.sub_nat(q, n))) -> N.Nat.Le(Nat.add(p, n), Nat.add(q, m)):
  match p m:
    case 0n 0n:
      %Equal.sym(Nat, Nat.add(q, 0n), q, N.Nat.add_zero(q)) : N.Nat.Le(Nat.add(0n, n), _)
      Int.le_pos_f(0n, q, n, h)
    case 0n 1n+mp:
      Int.le_negs_f(mp, q, n, h)
    case 1n+pp 0n:
      %Equal.sym(Nat, Nat.add(q, 0n), q, N.Nat.add_zero(q)) : N.Nat.Le(Nat.add(1n+pp, n), _)
      Int.le_pos_f(1n+pp, q, n, h)
    case 1n+pp 1n+mp:
      %Equal.sym(Nat, Nat.add(q, 1n+mp), 1n+Nat.add(q, mp), N.Nat.add_succ(q, mp)) : N.Nat.Le(Nat.add(1n+pp, n), _)
      Int.le_f(pp, mp, q, n, h)

def Int.le_pos_b(+x: Nat, q: Nat, n: Nat, h: N.Nat.Le(Nat.add(x, n), q)) -> C.Int.Le(C.Pos{x}, Int.sub_nat(q, n)):
  match q n:
    case 0n 0n:
      %N.Nat.add_zero(x) : N.Nat.Le(_, 0n)
      h
    case 0n 1n+np:
      Empty.absurd(C.Int.Le(C.Pos{x}, C.NegS{np}), Int.le_succ_zero(Nat.add(x, np), Int.le_cast(Nat.add(x, 1n+np), 1n+Nat.add(x, np), 0n, N.Nat.add_succ(x, np), h)))
    case 1n+qp 0n:
      %N.Nat.add_zero(x) : N.Nat.Le(_, 1n+qp)
      h
    case 1n+qp 1n+np:
      Int.le_pos_b(x, qp, np, Int.le_cast(Nat.add(x, 1n+np), 1n+Nat.add(x, np), 1n+qp, N.Nat.add_succ(x, np), h))

def Int.le_negs_b(+m: Nat, q: Nat, n: Nat, h: N.Nat.Le(n, Nat.add(q, 1n+m))) -> C.Int.Le(C.NegS{m}, Int.sub_nat(q, n)):
  match q n:
    case 0n 0n:
      Unit{}
    case 0n 1n+np:
      h
    case 1n+qp 0n:
      Unit{}
    case 1n+qp 1n+np:
      Int.le_negs_b(m, qp, np, h)

def Int.le_b(p: Nat, m: Nat, +q: Nat, +n: Nat, h: N.Nat.Le(Nat.add(p, n), Nat.add(q, m))) -> C.Int.Le(Int.sub_nat(p, m), Int.sub_nat(q, n)):
  match p m:
    case 0n 0n:
      Int.le_pos_b(0n, q, n, Int.le_cast_r(Nat.add(q, 0n), q, Nat.add(0n, n), N.Nat.add_zero(q), h))
    case 0n 1n+mp:
      Int.le_negs_b(mp, q, n, h)
    case 1n+pp 0n:
      Int.le_pos_b(1n+pp, q, n, Int.le_cast_r(Nat.add(q, 0n), q, Nat.add(1n+pp, n), N.Nat.add_zero(q), h))
    case 1n+pp 1n+mp:
      Int.le_b(pp, mp, q, n, Int.le_cast_r(Nat.add(q, 1n+mp), 1n+Nat.add(q, mp), Nat.add(1n+pp, n), N.Nat.add_succ(q, mp), h))

def Int.le_split(+a: C.Int, +b: C.Int, h: C.Int.Le(a, b)) -> C.Int.Le(Int.sub_nat(Int.toP(a), Int.toM(a)), Int.sub_nat(Int.toP(b), Int.toM(b))):
  %Equal.sym(C.Int, Int.sub_nat(Int.toP(a), Int.toM(a)), a, Int.split(a)) : C.Int.Le(_, Int.sub_nat(Int.toP(b), Int.toM(b)))
  %Equal.sym(C.Int, Int.sub_nat(Int.toP(b), Int.toM(b)), b, Int.split(b)) : C.Int.Le(a, _)
  h

def Int.le_neg.core(+pa: Nat, +ma: Nat, +pb: Nat, +mb: Nat, h: N.Nat.Le(Nat.add(pa, mb), Nat.add(pb, ma))) -> C.Int.Le(C.Int.neg(Int.sub_nat(pb, mb)), C.Int.neg(Int.sub_nat(pa, ma))):
  %Equal.sym(C.Int, C.Int.neg(Int.sub_nat(pb, mb)), Int.sub_nat(mb, pb), Int.neg_sub(pb, mb)) : C.Int.Le(_, C.Int.neg(Int.sub_nat(pa, ma)))
  %Equal.sym(C.Int, C.Int.neg(Int.sub_nat(pa, ma)), Int.sub_nat(ma, pa), Int.neg_sub(pa, ma)) : C.Int.Le(Int.sub_nat(mb, pb), _)
  Int.le_b(mb, pb, ma, pa,
    Int.le_cast_r(Nat.add(pb, ma), Nat.add(ma, pb), Nat.add(mb, pa), N.Nat.add_comm(pb, ma),
      Int.le_cast(Nat.add(pa, mb), Nat.add(mb, pa), Nat.add(pb, ma), N.Nat.add_comm(pa, mb), h)))

def C.le_neg(a, b, h):
  Int.by2(x => y => C.Int.Le(C.Int.neg(y), C.Int.neg(x)), a, b,
    Int.le_neg.core(Int.toP(a), Int.toM(a), Int.toP(b), Int.toM(b),
      Int.le_f(Int.toP(a), Int.toM(a), Int.toP(b), Int.toM(b), Int.le_split(a, b, h))))

def Int.le_add.core(+pa: Nat, +ma: Nat, +pb: Nat, +mb: Nat, +pc: Nat, +mc: Nat, h: N.Nat.Le(Nat.add(pa, mb), Nat.add(pb, ma))) -> C.Int.Le(C.Int.add(Int.sub_nat(pa, ma), Int.sub_nat(pc, mc)), C.Int.add(Int.sub_nat(pb, mb), Int.sub_nat(pc, mc))):
  %Equal.sym(C.Int, C.Int.add(Int.sub_nat(pa, ma), Int.sub_nat(pc, mc)), Int.sub_nat(Nat.add(pa, pc), Nat.add(ma, mc)), Int.add_sub(pa, ma, pc, mc)) : C.Int.Le(_, C.Int.add(Int.sub_nat(pb, mb), Int.sub_nat(pc, mc)))
  %Equal.sym(C.Int, C.Int.add(Int.sub_nat(pb, mb), Int.sub_nat(pc, mc)), Int.sub_nat(Nat.add(pb, pc), Nat.add(mb, mc)), Int.add_sub(pb, mb, pc, mc)) : C.Int.Le(Int.sub_nat(Nat.add(pa, pc), Nat.add(ma, mc)), _)
  Int.le_b(Nat.add(pa, pc), Nat.add(ma, mc), Nat.add(pb, pc), Nat.add(mb, mc),
    Int.le_cast_r(Nat.add(Nat.add(pb, ma), Nat.add(pc, mc)), Nat.add(Nat.add(pb, pc), Nat.add(ma, mc)), Nat.add(Nat.add(pa, pc), Nat.add(mb, mc)), N.Nat.add_add_swap(pb, ma, pc, mc),
      Int.le_cast(Nat.add(Nat.add(pa, mb), Nat.add(pc, mc)), Nat.add(Nat.add(pa, pc), Nat.add(mb, mc)), Nat.add(Nat.add(pb, ma), Nat.add(pc, mc)), N.Nat.add_add_swap(pa, mb, pc, mc),
        N.Nat.le_add_both(Nat.add(pa, mb), Nat.add(pb, ma), Nat.add(pc, mc), Nat.add(pc, mc), h, N.Nat.le_refl(Nat.add(pc, mc))))))

def C.le_add(a, b, c, h):
  Int.by3(x => y => z => C.Int.Le(C.Int.add(x, z), C.Int.add(y, z)), a, b, c,
    Int.le_add.core(Int.toP(a), Int.toM(a), Int.toP(b), Int.toM(b), Int.toP(c), Int.toM(c),
      Int.le_f(Int.toP(a), Int.toM(a), Int.toP(b), Int.toM(b), Int.le_split(a, b, h))))

# x <= y gives xc <= yc
def Int.le_mul_r(x: Nat, y: Nat, +c: Nat, h: N.Nat.Le(x, y)) -> N.Nat.Le(Nat.mul(x, c), Nat.mul(y, c)):
  match x y:
    case 0n 0n:
      Unit{}
    case 0n 1n+yp:
      Unit{}
    case 1n+xp 0n:
      match h:
    case 1n+xp 1n+yp:
      N.Nat.le_add_mono_l(c, Nat.mul(xp, c), Nat.mul(yp, c), Int.le_mul_r(xp, yp, c, h))

# (p - m) * k = pk - mk
def Int.mul_sub_r(+p: Nat, +m: Nat, +k: Nat) -> {C.Int.mul(Int.sub_nat(p, m), C.Pos{k}) == Int.sub_nat(Nat.mul(p, k), Nat.mul(m, k)) : C.Int}:
  %Equal.sym(C.Int, C.Int.mul(Int.sub_nat(p, m), C.Pos{k}), C.Int.mul(C.Pos{k}, Int.sub_nat(p, m)), C.mul_comm(Int.sub_nat(p, m), C.Pos{k})) : {_ == Int.sub_nat(Nat.mul(p, k), Nat.mul(m, k)) : C.Int}
  %Equal.sym(C.Int, C.Int.mul(C.Pos{k}, Int.sub_nat(p, m)), Int.sub_nat(Nat.mul(k, p), Nat.mul(k, m)), Int.mul_pos(k, p, m)) : {_ == Int.sub_nat(Nat.mul(p, k), Nat.mul(m, k)) : C.Int}
  %N.Nat.mul_comm(k, p) : {Int.sub_nat(Nat.mul(k, p), Nat.mul(k, m)) == Int.sub_nat(_, Nat.mul(m, k)) : C.Int}
  %N.Nat.mul_comm(k, m) : {Int.sub_nat(Nat.mul(k, p), Nat.mul(k, m)) == Int.sub_nat(Nat.mul(k, p), _) : C.Int}
  {==}

def Int.le_mul.core(+pa: Nat, +ma: Nat, +pb: Nat, +mb: Nat, +k: Nat, h: N.Nat.Le(Nat.add(pa, mb), Nat.add(pb, ma))) -> C.Int.Le(C.Int.mul(Int.sub_nat(pa, ma), C.Pos{k}), C.Int.mul(Int.sub_nat(pb, mb), C.Pos{k})):
  %Equal.sym(C.Int, C.Int.mul(Int.sub_nat(pa, ma), C.Pos{k}), Int.sub_nat(Nat.mul(pa, k), Nat.mul(ma, k)), Int.mul_sub_r(pa, ma, k)) : C.Int.Le(_, C.Int.mul(Int.sub_nat(pb, mb), C.Pos{k}))
  %Equal.sym(C.Int, C.Int.mul(Int.sub_nat(pb, mb), C.Pos{k}), Int.sub_nat(Nat.mul(pb, k), Nat.mul(mb, k)), Int.mul_sub_r(pb, mb, k)) : C.Int.Le(Int.sub_nat(Nat.mul(pa, k), Nat.mul(ma, k)), _)
  Int.le_b(Nat.mul(pa, k), Nat.mul(ma, k), Nat.mul(pb, k), Nat.mul(mb, k),
    Int.le_cast_r(Nat.mul(Nat.add(pb, ma), k), Nat.add(Nat.mul(pb, k), Nat.mul(ma, k)), Nat.add(Nat.mul(pa, k), Nat.mul(mb, k)), N.Nat.add_mul(pb, ma, k),
      Int.le_cast(Nat.mul(Nat.add(pa, mb), k), Nat.add(Nat.mul(pa, k), Nat.mul(mb, k)), Nat.mul(Nat.add(pb, ma), k), N.Nat.add_mul(pa, mb, k),
        Int.le_mul_r(Nat.add(pa, mb), Nat.add(pb, ma), k, h))))

def C.le_mul_nonneg(a, b, n, h):
  Int.by2(x => y => C.Int.Le(C.Int.mul(x, C.Pos{n}), C.Int.mul(y, C.Pos{n})), a, b,
    Int.le_mul.core(Int.toP(a), Int.toM(a), Int.toP(b), Int.toM(b), n,
      Int.le_f(Int.toP(a), Int.toM(a), Int.toP(b), Int.toM(b), Int.le_split(a, b, h))))

# ---- the sign/magnitude view (what multiplication really is) ------------

def Int.sgn(s: Bool, k: Nat) -> C.Int:
  match s:
    case True{}:
      C.Pos{k}
    case False{}:
      Int.neg_nat(k)

def Int.sign(a: C.Int) -> Bool:
  match a:
    case C.Pos{n}:
      True{}
    case C.NegS{n}:
      False{}

def Int.sgn_split(a: C.Int) -> {Int.sgn(Int.sign(a), C.Int.abs(a)) == a : C.Int}:
  match a:
    case C.Pos{n}:
      {==}
    case C.NegS{n}:
      {==}

def Int.mul_pos_neg(+k: Nat, j: Nat) -> {C.Int.mul(C.Pos{k}, Int.neg_nat(j)) == Int.neg_nat(Nat.mul(k, j)) : C.Int}:
  match j:
    case 0n:
      %Equal.sym(Nat, Nat.mul(k, 0n), 0n, N.Nat.mul_zero(k)) : {C.Pos{_} == Int.neg_nat(_) : C.Int}
      {==}
    case 1n+jp:
      {==}

def Int.mul_neg_pos(k: Nat, +j: Nat) -> {C.Int.mul(Int.neg_nat(k), C.Pos{j}) == Int.neg_nat(Nat.mul(k, j)) : C.Int}:
  match k:
    case 0n:
      {==}
    case 1n+kp:
      {==}

def Int.mul_neg_neg(k: Nat, j: Nat) -> {C.Int.mul(Int.neg_nat(k), Int.neg_nat(j)) == C.Pos{Nat.mul(k, j)} : C.Int}:
  match k j:
    case 0n 0n:
      {==}
    case 0n 1n+jp:
      {==}
    case 1n+kp 0n:
      %Equal.sym(Nat, Nat.mul(1n+kp, 0n), 0n, N.Nat.mul_zero(1n+kp)) : {Int.neg_nat(_) == C.Pos{_} : C.Int}
      {==}
    case 1n+kp 1n+jp:
      {==}

def Int.mul_sgn(s: Bool, t: Bool, +k: Nat, +j: Nat) -> {C.Int.mul(Int.sgn(s, k), Int.sgn(t, j)) == Int.sgn(N.Bool.same(s, t), Nat.mul(k, j)) : C.Int}:
  match s t:
    case True{} True{}:
      {==}
    case True{} False{}:
      Int.mul_pos_neg(k, j)
    case False{} True{}:
      Int.mul_neg_pos(k, j)
    case False{} False{}:
      Int.mul_neg_neg(k, j)

def Int.same_assoc(a: Bool, b: Bool, c: Bool) -> {N.Bool.same(a, N.Bool.same(b, c)) == N.Bool.same(N.Bool.same(a, b), c) : Bool}:
  match a b c:
    case True{} True{} True{}:
      {==}
    case True{} True{} False{}:
      {==}
    case True{} False{} True{}:
      {==}
    case True{} False{} False{}:
      {==}
    case False{} True{} True{}:
      {==}
    case False{} True{} False{}:
      {==}
    case False{} False{} True{}:
      {==}
    case False{} False{} False{}:
      {==}

def Int.sby3(-P: C.Int -> C.Int -> C.Int -> Type, +a: C.Int, +b: C.Int, +c: C.Int, w: P(Int.sgn(Int.sign(a), C.Int.abs(a)), Int.sgn(Int.sign(b), C.Int.abs(b)), Int.sgn(Int.sign(c), C.Int.abs(c)))) -> P(a, b, c):
  %Int.sgn_split(a) : P(_, b, c)
  %Int.sgn_split(b) : P(Int.sgn(Int.sign(a), C.Int.abs(a)), _, c)
  %Int.sgn_split(c) : P(Int.sgn(Int.sign(a), C.Int.abs(a)), Int.sgn(Int.sign(b), C.Int.abs(b)), _)
  w

def Int.mul_assoc.core(+sa: Bool, +ka: Nat, +sb: Bool, +kb: Nat, +sc: Bool, +kc: Nat) -> {C.Int.mul(Int.sgn(sa, ka), C.Int.mul(Int.sgn(sb, kb), Int.sgn(sc, kc))) == C.Int.mul(C.Int.mul(Int.sgn(sa, ka), Int.sgn(sb, kb)), Int.sgn(sc, kc)) : C.Int}:
  %Equal.sym(C.Int, C.Int.mul(Int.sgn(sb, kb), Int.sgn(sc, kc)), Int.sgn(N.Bool.same(sb, sc), Nat.mul(kb, kc)), Int.mul_sgn(sb, sc, kb, kc)) : {C.Int.mul(Int.sgn(sa, ka), _) == C.Int.mul(C.Int.mul(Int.sgn(sa, ka), Int.sgn(sb, kb)), Int.sgn(sc, kc)) : C.Int}
  %Equal.sym(C.Int, C.Int.mul(Int.sgn(sa, ka), Int.sgn(sb, kb)), Int.sgn(N.Bool.same(sa, sb), Nat.mul(ka, kb)), Int.mul_sgn(sa, sb, ka, kb)) : {C.Int.mul(Int.sgn(sa, ka), Int.sgn(N.Bool.same(sb, sc), Nat.mul(kb, kc))) == C.Int.mul(_, Int.sgn(sc, kc)) : C.Int}
  %Equal.sym(C.Int, C.Int.mul(Int.sgn(sa, ka), Int.sgn(N.Bool.same(sb, sc), Nat.mul(kb, kc))), Int.sgn(N.Bool.same(sa, N.Bool.same(sb, sc)), Nat.mul(ka, Nat.mul(kb, kc))), Int.mul_sgn(sa, N.Bool.same(sb, sc), ka, Nat.mul(kb, kc))) : {_ == C.Int.mul(Int.sgn(N.Bool.same(sa, sb), Nat.mul(ka, kb)), Int.sgn(sc, kc)) : C.Int}
  %Equal.sym(C.Int, C.Int.mul(Int.sgn(N.Bool.same(sa, sb), Nat.mul(ka, kb)), Int.sgn(sc, kc)), Int.sgn(N.Bool.same(N.Bool.same(sa, sb), sc), Nat.mul(Nat.mul(ka, kb), kc)), Int.mul_sgn(N.Bool.same(sa, sb), sc, Nat.mul(ka, kb), kc)) : {Int.sgn(N.Bool.same(sa, N.Bool.same(sb, sc)), Nat.mul(ka, Nat.mul(kb, kc))) == _ : C.Int}
  %Int.same_assoc(sa, sb, sc) : {Int.sgn(N.Bool.same(sa, N.Bool.same(sb, sc)), Nat.mul(ka, Nat.mul(kb, kc))) == Int.sgn(_, Nat.mul(Nat.mul(ka, kb), kc)) : C.Int}
  %N.Nat.mul_assoc(ka, kb, kc) : {Int.sgn(N.Bool.same(sa, N.Bool.same(sb, sc)), Nat.mul(ka, Nat.mul(kb, kc))) == Int.sgn(N.Bool.same(sa, N.Bool.same(sb, sc)), _) : C.Int}
  {==}

def C.mul_assoc(a, b, c):
  Int.sby3(x => y => z => {C.Int.mul(x, C.Int.mul(y, z)) == C.Int.mul(C.Int.mul(x, y), z) : C.Int}, a, b, c,
    Int.mul_assoc.core(Int.sign(a), C.Int.abs(a), Int.sign(b), C.Int.abs(b), Int.sign(c), C.Int.abs(c)))

# ---- no zero divisors ---------------------------------------------------

def Int.abs_neg_nat(k: Nat) -> {C.Int.abs(Int.neg_nat(k)) == k : Nat}:
  match k:
    case 0n:
      {==}
    case 1n+kp:
      {==}

def Int.abs_mul(a: C.Int, b: C.Int) -> {C.Int.abs(C.Int.mul(a, b)) == Nat.mul(C.Int.abs(a), C.Int.abs(b)) : Nat}:
  match a b:
    case C.Pos{x} C.Pos{y}:
      {==}
    case C.Pos{x} C.NegS{y}:
      Int.abs_neg_nat(Nat.mul(x, 1n+y))
    case C.NegS{x} C.Pos{y}:
      Int.abs_neg_nat(Nat.mul(1n+x, y))
    case C.NegS{x} C.NegS{y}:
      {==}

def Int.abs_zero(a: C.Int, e: {C.Int.abs(a) == 0n : Nat}) -> {a == C.Pos{0n} : C.Int}:
  match a:
    case C.Pos{n}:
      %e : {C.Pos{n} == C.Pos{_} : C.Int}
      {==}
    case C.NegS{n}:
      Empty.absurd({C.NegS{n} == C.Pos{0n} : C.Int}, N.Nat.succ_neq_zero(n, e))

def Int.mul_eq_zero_nat(x: Nat, +y: Nat, e: {Nat.mul(x, y) == 0n : Nat}, nx: {x == 0n : Nat} -> Empty) -> {y == 0n : Nat}:
  match x:
    case 0n:
      Empty.absurd({y == 0n : Nat}, nx({==}))
    case 1n+xp:
      N.Nat.add_eq_zero_l(y, Nat.mul(xp, y), e)

def C.mul_eq_zero(a, b, e, na):
  Int.abs_zero(b, Int.mul_eq_zero_nat(C.Int.abs(a), C.Int.abs(b),
    Equal.trans(Nat, Nat.mul(C.Int.abs(a), C.Int.abs(b)), C.Int.abs(C.Int.mul(a, b)), 0n,
      Equal.sym(Nat, C.Int.abs(C.Int.mul(a, b)), Nat.mul(C.Int.abs(a), C.Int.abs(b)), Int.abs_mul(a, b)),
      Equal.cong(C.Int, Nat, z => C.Int.abs(z), C.Int.mul(a, b), C.Pos{0n}, e)),
    k => na(Int.abs_zero(a, k))))