module Int

import UInt
import Base

import IntDefs
import IntAddSub
import IntLess

/*
  Theorems about Int multiplication.

  Multiplication is defined by combining signs and multiplying
  absolute values; these proofs establish the expected sign cases and
  algebraic laws.
*/

// Properties of Multiplication

lemma mult_pos_pos: all x:UInt, y:UInt. pos(x) * pos(y) = pos(x * y)
proof
  arbitrary x:UInt, y:UInt
  evaluate
end

lemma mult_pos_negsuc: all x:UInt, y:UInt.
  pos(x) * negsuc(y) = - pos(x + x * y)
proof
  arbitrary x:UInt, y:UInt
  show #pos(x) * negsuc(y)# = - pos(x + x * y)
  expand operator*
  expand sign | abs
  replace mult_pos_neg | mult_neg_uint | uint_dist_mult_add.
end

theorem int_one_mult: all x:Int. +1 * x = x
proof
  arbitrary x:Int
  switch x {
    case pos(x') {
      replace mult_pos_pos.
    }
    case negsuc(x') {
      replace mult_pos_negsuc | neg_pos.
    }
  }
end

auto int_one_mult

theorem int_zero_mult: all x:Int. +0 * x = +0
proof
  arbitrary x:Int
  switch x {
    case pos(x') {
      expand operator* | sign | abs | 2*operator*.
    }
    case negsuc(x') {
      expand operator* | sign | abs | 2*operator* | operator-.
    }
  }
end

auto int_zero_mult

lemma sign_neg_flip: all x:Int.
  if not (x = +0)
  then sign(- x) = flip(sign(x))
proof
  arbitrary x:Int
  switch x {
    case pos(x') {
      assume prem
      expand operator-
      have xnz: not (x' = 0) by {
        assume xz
        conclude false by replace xz in prem
      }
      simplify with xnz
      expand sign | flip.
    }
    case negsuc(x') {
      expand operator- | sign | flip.
    }
  }
end

theorem dist_neg_mult: all x:Int,y:Int.
  -(x * y) = (-x) * y
proof
  arbitrary x:Int, y:Int
  switch x {
    case pos(x') {
      switch y {
        case pos(y') {
          expand operator* 
          replace sign_pos
          replace mult_pos_any | abs_pos | mult_pos_uint
          cases uint_zero_or_positive[x']
          case xz {
            replace xz | neg_zero
            expand sign | abs
            replace mult_pos_any | mult_pos_uint.
          }
          case xp_pos {
            have xnz: not (x' = 0) by apply uint_pos_not_zero to xp_pos
            expand operator-
            simplify with xnz
            expand abs | sign
            replace mult_neg_pos | mult_neg_uint
            cases uint_zero_or_positive[y']
            case yz {
              replace yz
              expand operator-.
            }
            case y_pos {
              have ynz: not (y' = 0) by apply uint_pos_not_zero to y_pos
              have nxyz: not (x' * y' = 0) by {
                assume xyz
                cases apply uint_mult_to_zero[x',y'] to xyz
                case xz {
                  conclude false by apply xnz to xz
                }
                case yz {
                  conclude false by apply ynz to yz
                }
              }
              simplify with nxyz
              have one_x: 1 ≤ x' by apply uint_pos_implies_one_le to xp_pos
              replace (apply uint_monus_add_identity to one_x)
              replace (symmetric neg_pos[(x' * y' ∸ 1)])
              have one_xy: 1 ≤ x' * y' by {
                obtain y'' where yp: y' = 1 + y'' from apply uint_positive_add_one to y_pos
                replace yp | uint_dist_mult_add
                have x_xy: x' ≤ x' + x' * y'' by uint_less_equal_add
                apply uint_less_equal_trans to one_x, x_xy
              }
              replace (apply uint_monus_add_identity to one_xy).
            }
          }
        }
        case negsuc(y') {
          expand operator*
          replace sign_pos | sign_negsuc | mult_pos_any | mult_neg_uint | abs_negsuc | abs_pos
          | neg_involutive | abs_neg | abs_pos
          cases uint_zero_or_positive[x']
          case xz {
            replace xz
            evaluate
          }
          case xp_pos {
            have xnz: not (x' = 0) by apply uint_pos_not_zero to xp_pos
            expand operator-
            simplify with xnz
            replace sign_negsuc | mult_neg_neg | mult_pos_uint.
          }
        }
      }
    }
    case negsuc(x') {
      switch y {
        case pos(y') {
          expand operator*
          replace sign_negsuc | sign_pos | abs_negsuc | abs_pos | mult_neg_pos | mult_neg_uint
          replace sign_neg_negsuc | mult_pos_any | abs_neg | abs_negsuc | mult_pos_uint | neg_involutive.
        }
        case negsuc(y') {
          expand operator*
          replace sign_negsuc | abs_negsuc | sign_neg_negsuc | mult_pos_neg | abs_neg | abs_negsuc | mult_neg_uint
            | mult_neg_neg | mult_pos_uint.
        }
      }
    }
  }
end

theorem int_mult_commute: all x:Int, y:Int. x * y = y * x
proof
  arbitrary x:Int, y:Int
  switch x {
    case pos(x') {
      switch y {
        case pos(y') {
          suffices pos(x' * y') = pos(y' * x')  by evaluate
          replace uint_mult_commute[x',y'].
        }
        case negsuc(y') {
          suffices - (x' * (1 + y')) = - ((1 + y') * x')  by evaluate
          replace uint_mult_commute[x', 1 + y'].
        }
      }
    }
    case negsuc(x') {
      switch y {
        case pos(y') {
          suffices - ((1 + x') * y') = - (y' * (1 + x'))  by evaluate
          replace uint_mult_commute[1 + x', y'].
        }
        case negsuc(y') {
          suffices pos((1 + x') * (1 + y')) = pos((1 + y') * (1 + x')) by evaluate
          replace uint_mult_commute[(1 + x'), (1 + y')].
        }
      }
    }
  }
end

theorem int_mult_one: all x:Int. x * +1 = x
proof
  arbitrary x:Int
  conclude x * +1 = x    by int_mult_commute[x,+1]
end

auto int_mult_one

theorem int_mult_zero: all x:Int. x * +0 = +0
proof
  arbitrary x:Int
  conclude x * +0 = +0  by int_mult_commute[x,+0]
end

auto int_mult_zero

lemma mult_assoc_helper: all x:UInt, y:UInt, z:UInt.
  z + (y + x * (1 + y)) * (1 + z)
  = (z + y * (1 + z)) + x * (1 + z + y * (1 + z))
proof
  arbitrary x:UInt, y:UInt, z:UInt
  equations
      z + (y + x * (1 + y)) * (1 + z)
    = z + (y + x + x * y) * (1 + z)
      by replace uint_dist_mult_add[x].
... = z + y + x + x * y + (y + x + x * y) * z
      by replace uint_dist_mult_add.
... = z + y + x + x * y + y*z + x*z + x*y*z
      by replace uint_dist_mult_add_right.
... = z + y + x + y*z + x*y + x*z + x*y*z
      by replace uint_add_commute[x*y, y*z].
... = z + y + x + y*z + x*z + x*y + x*y*z
      by replace uint_add_commute[x*y].
... = z + y + y*z + x + x*z + x*y + x*y*z
      by replace uint_add_commute[x].
... = #(z + y * (1 + z)) + x * (1 + z + y * (1 + z))#
      by replace uint_dist_mult_add.
end

theorem int_mult_assoc: all x:Int, y:Int, z:Int. (x * y) * z = x * (y * z)
proof
  arbitrary x:Int, y:Int, z:Int
  switch x {
    case pos(x') {
      cases uint_zero_or_positive[x']
      case xpz: x' = 0 {
        replace xpz.
      }
      case xp_pos: 0 < x' {
        have xnz: not (x' = 0) by apply uint_pos_not_zero to xp_pos
        obtain x'' where xp_eq: x' = 1 + x'' from apply uint_positive_add_one to xp_pos
        switch y {
          case pos(y') {
            cases uint_zero_or_positive[y']
            case ypz: y' = 0 {
              replace ypz.
            }
            case yp_pos: 0 < y' {
              have ynz: not (y' = 0) by apply uint_pos_not_zero to yp_pos
              switch z {
                case pos(z') {
                  replace mult_pos_pos | mult_pos_pos.
                }
                case negsuc(z') {
                  replace mult_pos_pos
                  replace mult_pos_negsuc
                  replace int_mult_commute[pos(x'), -pos(y'+y'*z')] | symmetric dist_neg_mult[pos(y'+y'*z'), pos(x')]
                  replace mult_pos_pos | uint_dist_mult_add_right | uint_mult_commute[y',x']
                  | uint_mult_commute[y'*z',x'].
                }
              }
            }
          }
          case negsuc(y') {
            switch z {
              case pos(z') {
                expand operator*
                replace sign_pos | sign_negsuc | abs_pos | abs_negsuc | mult_pos_neg | mult_neg_uint
                replace mult_neg_pos | mult_neg_uint | abs_neg | abs_pos | mult_any_pos | mult_pos_any
                replace uint_dist_mult_add | uint_dist_mult_add_right
                replace xp_eq | sign_neg_pos
                
                cases uint_zero_or_positive[z']
                case zpz: z' = 0 {
                  replace zpz
                  expand operator- | sign | 2*operator* | operator-.
                }
                case zp_pos: 0 < z' {
                  have znz: not (z' = 0) by apply uint_pos_not_zero to zp_pos
                  obtain z'' where zp_eq: z' = 1 + z'' from apply uint_positive_add_one to zp_pos
                  replace zp_eq
                  replace sign_neg_pos.
                }
              }
              case negsuc(z') {
                expand operator*
                replace sign_pos | sign_negsuc | abs_pos | abs_negsuc
                replace mult_pos_neg | mult_neg_uint | mult_pos_any | mult_neg_neg | mult_pos_uint | abs_pos | sign_pos
                replace mult_pos_uint | uint_dist_mult_add | uint_dist_mult_add
                replace xp_eq | sign_neg_pos | mult_neg_neg | abs_neg | abs_pos | mult_pos_uint.
              }
            }
          }
        }
      }
    }
    case negsuc(x') {
      switch y {
        case pos(y') {
          switch z {
            case pos(z') {
              expand operator*
              replace sign_negsuc | sign_pos | abs_negsuc | abs_pos | mult_neg_pos | mult_neg_uint | mult_pos_any
              | mult_pos_uint | uint_dist_mult_add_right | sign_pos | mult_neg_pos | abs_pos
              | mult_neg_uint
              cases uint_zero_or_positive[y']
              case ypz: y' = 0 {
                replace ypz
                expand operator- | abs | sign | 2* operator*.
              }
              case yp_pos: 0 < y' {
                obtain y'' where yp_eq: y' = 1 + y'' from apply uint_positive_add_one to yp_pos
                replace yp_eq
                replace sign_neg_pos | mult_neg_pos | abs_neg | abs_pos | mult_neg_uint | uint_dist_mult_add_right
                | uint_dist_mult_add | uint_dist_mult_add_right | uint_dist_mult_add_right.
              }
            }
            case negsuc(z') {
              expand operator*
              replace sign_negsuc | sign_pos | abs_negsuc | abs_pos | mult_neg_pos | mult_neg_uint | mult_pos_neg
              | mult_neg_uint | uint_dist_mult_add_right | uint_dist_mult_add
              cases uint_zero_or_positive[y']
              case ypz: y' = 0 {
                replace ypz
                expand operator-
                expand sign | abs
                evaluate
              }
              case yp_pos: 0 < y' {
                obtain y'' where yp_eq: y' = 1 + y'' from apply uint_positive_add_one to yp_pos
                replace yp_eq
                replace sign_neg_pos | abs_neg | abs_pos | mult_neg_neg | uint_dist_mult_add
                replace uint_dist_mult_add_right | mult_pos_uint
                replace uint_add_commute[x'+x'*y'',z']
                replace uint_add_commute[x'+x'*y'',y''*z'].
              }
            }
          }
            }
            case negsuc(y') {
              switch z {
                case pos(z') {
                  cases uint_zero_or_positive[z']
                  case zpz: z' = 0 {
                    replace zpz
                    evaluate
                  }
                  case zp_pos: 0 < z' {
                    have znz: not (z' = 0) by apply uint_pos_not_zero to zp_pos
                    obtain z'' where zp_eq: z' = 1 + z'' from apply uint_positive_add_one to zp_pos
                    replace zp_eq
                    expand operator*
                    replace sign_negsuc | abs_negsuc | mult_neg_neg | sign_pos | mult_pos_uint | mult_neg_pos | abs_pos
                    | mult_neg_uint | sign_pos | mult_pos_any | uint_dist_mult_add
                    | uint_dist_mult_add_right
                    | uint_dist_mult_add_right
                    | uint_dist_mult_add
                    | sign_neg_pos | mult_neg_neg | mult_pos_uint | abs_neg | abs_pos
                    | uint_add_commute[z'' + x' + x' * z'', y']
                    | uint_add_commute[x' + x' * z'', y' * z'']
                    | uint_dist_mult_add
                    | uint_add_commute[x' * z'', x' * y'].
                  }
                }
                case negsuc(z'') {
                  suffices negsuc(z'' + (y' + x' * (1 + y')) * (1 + z''))
                         = negsuc((z'' + y' * (1 + z'')) + x' * (1 + z'' + y' * (1 + z'')))
                    by evaluate
                  replace mult_assoc_helper[x',y',z''].
                }
              }
            }
          }      
    }
  }
end

associative operator* in Int

// Helper: pos(a) distributes over the signed-difference operator ⊝.
lemma mult_pos_monuso: all a:UInt, m:UInt, n:UInt.
  pos(a) * (m ⊝ n) = (a * m) ⊝ (a * n)
proof
  arbitrary a:UInt, m:UInt, n:UInt
  cases uint_zero_or_positive[a]
  case a_zero: a = 0 {
    replace a_zero | int_monuso_cancel
    int_zero_mult[m ⊝ n]
  }
  case a_pos: 0 < a {
    switch m < n for operator⊝ {
      case true assume m_lt_n {
        have am_lt_an: a * m < a * n
          by apply uint_pos_mult_both_sides_of_less[a, m, n] to a_pos, m_lt_n
        simplify with am_lt_an
        replace neg_uint
        replace symmetric uint_dist_mult_monus[a, n, m]
        equations
              pos(a) * -pos(n ∸ m)
            = -pos(n ∸ m) * pos(a)         by int_mult_commute[pos(a), -pos(n ∸ m)]
        ... = -(pos(n ∸ m) * pos(a))       by symmetric dist_neg_mult[pos(n ∸ m), pos(a)]
        ... = -(pos(a) * pos(n ∸ m))       by replace int_mult_commute[pos(n ∸ m), pos(a)].
        ... = -pos(a * (n ∸ m))            by replace mult_pos_pos.
      }
      case false assume not_m_lt_n {
        have n_le_m: n ≤ m by apply uint_not_less_implies_less_equal[m, n] to not_m_lt_n
        have an_le_am: a * n ≤ a * m by apply uint_mult_mono_le[a, n, m] to n_le_m
        have not_am_lt_an: not (a * m < a * n) by {
          assume am_lt_an
          have alt: a * n < a * m or a * n = a * m  by expand operator≤ in an_le_am
          cases alt
          case an_lt_am {
            have an_lt_an: a * n < a * n
              by apply uint_less_trans[a*n, a*m, a*n] to an_lt_am, am_lt_an
            apply uint_less_irreflexive[a*n] to an_lt_an
          }
          case an_eq_am {
            have an_lt_an: a * n < a * n by replace an_eq_am in am_lt_an
            apply uint_less_irreflexive[a*n] to an_lt_an
          }
        }
        simplify with not_am_lt_an
        replace mult_pos_pos | uint_dist_mult_monus.
      }
    }
  }
end

// Helper: distributivity when the multiplicand is `pos(a)`.
lemma mult_pos_dist_add: all a:UInt. all x:Int, y:Int.
  pos(a) * (x + y) = pos(a) * x + pos(a) * y
proof
  arbitrary a:UInt, x:Int, y:Int
  switch x {
    case pos(x') {
      switch y {
        case pos(y') {
          replace add_pos_pos
          replace mult_pos_pos
          replace add_pos_pos
          replace uint_dist_mult_add.
        }
        case negsuc(y') {
          replace add_pos_negsuc | mult_pos_pos | mult_pos_negsuc
          replace mult_pos_monuso[a, x', 1 + y']
          replace uint_dist_mult_add[a, 1, y']
          replace subo_monus
          expand 2*operator-.
        }
      }
    }
    case negsuc(x') {
      switch y {
        case pos(y') {
          replace add_negsuc_pos | mult_pos_negsuc | mult_pos_pos
          replace mult_pos_monuso[a, y', 1 + x']
          replace uint_dist_mult_add[a, 1, x']
          replace subo_monus
          expand 2*operator-
          int_add_commute
        }
        case negsuc(y') {
          replace add_negsuc_negsuc | mult_pos_negsuc
          replace symmetric neg_distr_add[pos(a + a * x'), pos(a + a * y')]
          replace add_pos_pos
          replace uint_dist_mult_add[a, 1 + x', y']
            | uint_dist_mult_add[a, 1, x']
            | uint_add_commute[a * x', a].
        }
      }
    }
  }
end

// Left distributivity of `*` over `+` on `Int`.
theorem int_dist_mult_add: all a:Int, x:Int, y:Int.
  a * (x + y) = a * x + a * y
proof
  arbitrary a:Int, x:Int, y:Int
  switch a {
    case pos(a') {
      mult_pos_dist_add[a', x, y]
    }
    case negsuc(a') {
      have ng_a: negsuc(a') = -pos(1 + a') by symmetric neg_pos[a']
      replace ng_a
      equations
            -pos(1 + a') * (x + y)
          = -(pos(1 + a') * (x + y))                    by symmetric dist_neg_mult[pos(1 + a'), x + y]
      ... = -(pos(1 + a') * x + pos(1 + a') * y)        by replace mult_pos_dist_add[1 + a', x, y].
      ... = -(pos(1 + a') * x) + -(pos(1 + a') * y)     by neg_distr_add[pos(1 + a') * x, pos(1 + a') * y]
      ... = -pos(1 + a') * x + -(pos(1 + a') * y)       by replace dist_neg_mult[pos(1 + a'), x].
      ... = -pos(1 + a') * x + -pos(1 + a') * y         by replace dist_neg_mult[pos(1 + a'), y].
    }
  }
end

// Right distributivity of `*` over `+` on `Int`.
theorem int_dist_mult_add_right: all a:Int, x:Int, y:Int.
  (x + y) * a = x * a + y * a
proof
  arbitrary a:Int, x:Int, y:Int
  replace int_mult_commute[x + y, a]
        | int_mult_commute[x, a]
        | int_mult_commute[y, a]
  int_dist_mult_add[a, x, y]
end

// Nonneg × nonneg is nonneg.
lemma int_nonneg_mult_nonneg: all a:Int, b:Int.
  if +0 ≤ a and +0 ≤ b
  then +0 ≤ a * b
proof
  arbitrary a:Int, b:Int
  switch a {
    case pos(au) {
      switch b {
        case pos(bu) {
          replace mult_pos_pos
          show +0 ≤ pos(au * bu)
          uint_zero_le[au * bu]
        }
        case negsuc(bu) { . }
      }
    }
    case negsuc(au) { . }
  }
end

// Pos × pos is positive.
lemma int_pos_mult_pos: all a:Int, b:Int.
  if +0 < a and +0 < b
  then +0 < a * b
proof
  arbitrary a:Int, b:Int
  switch a {
    case pos(au) {
      switch b {
        case pos(bu) {
          assume prem
          have zlt_au: 0 < au by conjunct 0 of prem
          have zlt_bu: 0 < bu by conjunct 1 of prem
          replace mult_pos_pos
          show +0 < pos(au * bu)
          apply uint_pos_mult_both_sides_of_less[au, 0, bu] to zlt_au, zlt_bu
        }
        case negsuc(bu) { . }
      }
    }
    case negsuc(au) { . }
  }
end

// Left distributivity of `*` over `-` on `Int`.
theorem int_dist_mult_sub: all a:Int, x:Int, y:Int.
  a * (x - y) = a * x - a * y
proof
  arbitrary a:Int, x:Int, y:Int
  have neg_mult_swap: a * (-y) = -(a * y) by {
    equations
          a * (-y)
        = (-y) * a          by int_mult_commute[a, -y]
    ... = -(y * a)          by symmetric dist_neg_mult[y, a]
    ... = -(a * y)          by replace int_mult_commute[y, a].
  }
  expand operator-
  show a * (x + -y) = a * x + -(a * y)
  replace int_dist_mult_add[a, x, -y]
  replace neg_mult_swap.
end

// Strict-inequality counterpart of `int_le_iff_diff_nonneg`:
// `x < y` is equivalent to the difference `y - x` being positive.
theorem int_less_iff_diff_pos: all a:Int, b:Int.
  a < b ⇔ +0 < b - a
proof
  arbitrary a:Int, b:Int
  have fwd: if a < b then +0 < b - a by {
    assume alb
    have a_le_b: a ≤ b by apply int_less_implies_less_equal[a, b] to alb
    have a_ne_b: not (a = b) by apply int_less_implies_not_equal[a, b] to alb
    have z_le_diff: +0 ≤ b - a
      by apply (conjunct 0 of int_le_iff_diff_nonneg[a, b]) to a_le_b
    have z_ne_diff: not (+0 = b - a) by {
      assume z_eq_diff
      have diff_z: b - a = +0 by symmetric z_eq_diff
      have b_eq_a: b = a by {
        have h1: b + -a = +0 by expand operator- in diff_z
        have h2: a + -a = +0 by int_add_inverse[a]
        have h3: b + -a = a + -a by transitive h1 (symmetric h2)
        apply int_add_both_sides_of_equal_right[-a, b, a] to h3
      }
      apply a_ne_b to symmetric b_eq_a
    }
    have le_or_eq: +0 < b - a or +0 = b - a
      by apply int_less_equal_implies_less_or_equal[+0, b - a] to z_le_diff
    cases le_or_eq
    case lt { lt }
    case eq { conclude false by apply z_ne_diff to eq }
  }
  have bkwd: if +0 < b - a then a < b by {
    assume zlt_diff
    have zle_diff: +0 ≤ b - a
      by apply int_less_implies_less_equal[+0, b - a] to zlt_diff
    have a_le_b: a ≤ b
      by apply (conjunct 1 of int_le_iff_diff_nonneg[a, b]) to zle_diff
    have a_ne_b: not (a = b) by {
      assume a_eq_b
      have diff_z: b - a = +0 by {
        replace a_eq_b
        int_sub_cancel[b]
      }
      have bad: +0 < +0 by replace diff_z in zlt_diff
      apply int_less_irreflexive[+0] to bad
    }
    have le_or_eq: a < b or a = b
      by apply int_less_equal_implies_less_or_equal[a, b] to a_le_b
    cases le_or_eq
    case lt { lt }
    case eq { conclude false by apply a_ne_b to eq }
  }
  fwd, bkwd
end

// Multiplication on the left by a nonneg Int preserves `≤`.
theorem int_nonneg_mult_mono_le_left: all n:Int, x:Int, y:Int.
  if +0 ≤ n and x ≤ y
  then n * x ≤ n * y
proof
  arbitrary n:Int, x:Int, y:Int
  assume prem
  have nn: +0 ≤ n by conjunct 0 of prem
  have xy: x ≤ y by conjunct 1 of prem
  have diff_nn: +0 ≤ y - x
    by apply (conjunct 0 of int_le_iff_diff_nonneg[x, y]) to xy
  have prod_nn: +0 ≤ n * (y - x)
    by apply int_nonneg_mult_nonneg[n, y - x] to nn, diff_nn
  have dist_sub: n * (y - x) = n * y - n * x by int_dist_mult_sub[n, y, x]
  have prod_nn2: +0 ≤ n * y - n * x by replace dist_sub in prod_nn
  apply (conjunct 1 of int_le_iff_diff_nonneg[n * x, n * y]) to prod_nn2
end

// Multiplication on the right by a nonneg Int preserves `≤`.
theorem int_nonneg_mult_mono_le_right: all n:Int, x:Int, y:Int.
  if +0 ≤ n and x ≤ y
  then x * n ≤ y * n
proof
  arbitrary n:Int, x:Int, y:Int
  assume prem
  have step: n * x ≤ n * y by apply int_nonneg_mult_mono_le_left[n, x, y] to prem
  replace int_mult_commute[n, x] | int_mult_commute[n, y] in step
end

// Multiplication on the left by a positive Int preserves `<`.
theorem int_pos_mult_mono_less_left: all n:Int, x:Int, y:Int.
  if +0 < n and x < y
  then n * x < n * y
proof
  arbitrary n:Int, x:Int, y:Int
  assume prem
  have zn: +0 < n by conjunct 0 of prem
  have xy: x < y by conjunct 1 of prem
  have diff_pos: +0 < y - x
    by apply (conjunct 0 of int_less_iff_diff_pos[x, y]) to xy
  have prod_pos: +0 < n * (y - x)
    by apply int_pos_mult_pos[n, y - x] to zn, diff_pos
  have dist_sub: n * (y - x) = n * y - n * x by int_dist_mult_sub[n, y, x]
  have prod_pos2: +0 < n * y - n * x by replace dist_sub in prod_pos
  apply (conjunct 1 of int_less_iff_diff_pos[n * x, n * y]) to prod_pos2
end

// Multiplication on the right by a positive Int preserves `<`.
theorem int_pos_mult_mono_less_right: all n:Int, x:Int, y:Int.
  if +0 < n and x < y
  then x * n < y * n
proof
  arbitrary n:Int, x:Int, y:Int
  assume prem
  have step: n * x < n * y by apply int_pos_mult_mono_less_left[n, x, y] to prem
  replace int_mult_commute[n, x] | int_mult_commute[n, y] in step
end

// Multiplication on the left by a non-positive Int reverses `≤`.
theorem int_nonpos_mult_mono_le_left: all n:Int, x:Int, y:Int.
  if n ≤ +0 and x ≤ y
  then n * y ≤ n * x
proof
  arbitrary n:Int, x:Int, y:Int
  assume prem
  have npos: n ≤ +0 by conjunct 0 of prem
  have xy: x ≤ y by conjunct 1 of prem
  have neg_n_nn0: -+0 ≤ -n by apply int_neg_le_mono[n, +0] to npos
  have neg_n_nn: +0 ≤ -n by replace neg_zero in neg_n_nn0
  have neg_n_mult: (-n) * x ≤ (-n) * y
    by apply int_nonneg_mult_mono_le_left[-n, x, y] to neg_n_nn, xy
  have eq_x: (-n) * x = -(n * x) by symmetric dist_neg_mult[n, x]
  have eq_y: (-n) * y = -(n * y) by symmetric dist_neg_mult[n, y]
  have neg_step: -(n * x) ≤ -(n * y) by replace eq_x | eq_y in neg_n_mult
  apply (conjunct 1 of int_neg_le_iff[n * y, n * x]) to neg_step
end

// Multiplication on the right by a non-positive Int reverses `≤`.
theorem int_nonpos_mult_mono_le_right: all n:Int, x:Int, y:Int.
  if n ≤ +0 and x ≤ y
  then y * n ≤ x * n
proof
  arbitrary n:Int, x:Int, y:Int
  assume prem
  have step: n * y ≤ n * x by apply int_nonpos_mult_mono_le_left[n, x, y] to prem
  replace int_mult_commute[n, x] | int_mult_commute[n, y] in step
end

// Multiplication on the left by a negative Int reverses `<`.
theorem int_neg_mult_mono_less_left: all n:Int, x:Int, y:Int.
  if n < +0 and x < y
  then n * y < n * x
proof
  arbitrary n:Int, x:Int, y:Int
  assume prem
  have nneg: n < +0 by conjunct 0 of prem
  have xy: x < y by conjunct 1 of prem
  have neg_n_pos0: -+0 < -n by apply int_neg_less_mono[n, +0] to nneg
  have neg_n_pos: +0 < -n by replace neg_zero in neg_n_pos0
  have neg_n_mult: (-n) * x < (-n) * y
    by apply int_pos_mult_mono_less_left[-n, x, y] to neg_n_pos, xy
  have eq_x: (-n) * x = -(n * x) by symmetric dist_neg_mult[n, x]
  have eq_y: (-n) * y = -(n * y) by symmetric dist_neg_mult[n, y]
  have neg_step: -(n * x) < -(n * y) by replace eq_x | eq_y in neg_n_mult
  apply (conjunct 1 of int_neg_less_iff[n * y, n * x]) to neg_step
end

// Multiplication on the right by a negative Int reverses `<`.
theorem int_neg_mult_mono_less_right: all n:Int, x:Int, y:Int.
  if n < +0 and x < y
  then y * n < x * n
proof
  arbitrary n:Int, x:Int, y:Int
  assume prem
  have step: n * y < n * x by apply int_neg_mult_mono_less_left[n, x, y] to prem
  replace int_mult_commute[n, x] | int_mult_commute[n, y] in step
end

// Left cancellation by a positive Int under `<`.
theorem int_pos_mult_left_cancel_less: all n:Int, x:Int, y:Int.
  if +0 < n and n * x < n * y
  then x < y
proof
  arbitrary n:Int, x:Int, y:Int
  assume prem
  have zn: +0 < n by conjunct 0 of prem
  have nxny: n * x < n * y by conjunct 1 of prem
  have tri: x < y or x = y or y < x by int_trichotomy[x, y]
  cases tri
  case x_l_y: x < y { x_l_y }
  case x_eq_y: x = y {
    have nx_eq_ny: n * x = n * y by replace x_eq_y.
    have bad: n * y < n * y by replace nx_eq_ny in nxny
    conclude false by apply int_less_irreflexive[n * y] to bad
  }
  case y_l_x: y < x {
    have ny_l_nx: n * y < n * x
      by apply int_pos_mult_mono_less_left[n, y, x] to zn, y_l_x
    have bad: n * y < n * y
      by apply int_less_trans[n * y, n * x, n * y] to ny_l_nx, nxny
    conclude false by apply int_less_irreflexive[n * y] to bad
  }
end

// Right cancellation by a positive Int under `<`.
theorem int_pos_mult_right_cancel_less: all n:Int, x:Int, y:Int.
  if +0 < n and x * n < y * n
  then x < y
proof
  arbitrary n:Int, x:Int, y:Int
  assume prem
  have zn: +0 < n by conjunct 0 of prem
  have xnyn: x * n < y * n by conjunct 1 of prem
  have nxny: n * x < n * y
    by replace int_mult_commute[n, x] | int_mult_commute[n, y]
       xnyn
  apply int_pos_mult_left_cancel_less[n, x, y] to zn, nxny
end

// Left cancellation by a positive Int under `≤`.
theorem int_pos_mult_left_cancel_le: all n:Int, x:Int, y:Int.
  if +0 < n and n * x ≤ n * y
  then x ≤ y
proof
  arbitrary n:Int, x:Int, y:Int
  assume prem
  have zn: +0 < n by conjunct 0 of prem
  have nxny: n * x ≤ n * y by conjunct 1 of prem
  have tri: x < y or x = y or y < x by int_trichotomy[x, y]
  cases tri
  case x_l_y: x < y {
    apply int_less_implies_less_equal[x, y] to x_l_y
  }
  case x_eq_y: x = y {
    replace symmetric x_eq_y
    int_less_equal_refl[x]
  }
  case y_l_x: y < x {
    have ny_l_nx: n * y < n * x
      by apply int_pos_mult_mono_less_left[n, y, x] to zn, y_l_x
    have bad: n * y < n * y
      by apply int_less_trans_less_equal_right[n * y, n * x, n * y]
         to ny_l_nx, nxny
    conclude false by apply int_less_irreflexive[n * y] to bad
  }
end

// Right cancellation by a positive Int under `≤`.
theorem int_pos_mult_right_cancel_le: all n:Int, x:Int, y:Int.
  if +0 < n and x * n ≤ y * n
  then x ≤ y
proof
  arbitrary n:Int, x:Int, y:Int
  assume prem
  have zn: +0 < n by conjunct 0 of prem
  have xnyn: x * n ≤ y * n by conjunct 1 of prem
  have nxny: n * x ≤ n * y
    by replace int_mult_commute[n, x] | int_mult_commute[n, y]
       xnyn
  apply int_pos_mult_left_cancel_le[n, x, y] to zn, nxny
end

// Left cancellation by a negative Int under `<` (reverses order).
theorem int_neg_mult_left_cancel_less: all n:Int, x:Int, y:Int.
  if n < +0 and n * x < n * y
  then y < x
proof
  arbitrary n:Int, x:Int, y:Int
  assume prem
  have nn: n < +0 by conjunct 0 of prem
  have nxny: n * x < n * y by conjunct 1 of prem
  have tri: y < x or y = x or x < y by int_trichotomy[y, x]
  cases tri
  case y_l_x: y < x { y_l_x }
  case y_eq_x: y = x {
    have nx_eq_ny: n * x = n * y by replace y_eq_x.
    have bad: n * y < n * y by replace nx_eq_ny in nxny
    conclude false by apply int_less_irreflexive[n * y] to bad
  }
  case x_l_y: x < y {
    have ny_l_nx: n * y < n * x
      by apply int_neg_mult_mono_less_left[n, x, y] to nn, x_l_y
    have bad: n * y < n * y
      by apply int_less_trans[n * y, n * x, n * y] to ny_l_nx, nxny
    conclude false by apply int_less_irreflexive[n * y] to bad
  }
end

// Right cancellation by a negative Int under `<` (reverses order).
theorem int_neg_mult_right_cancel_less: all n:Int, x:Int, y:Int.
  if n < +0 and x * n < y * n
  then y < x
proof
  arbitrary n:Int, x:Int, y:Int
  assume prem
  have nn: n < +0 by conjunct 0 of prem
  have xnyn: x * n < y * n by conjunct 1 of prem
  have nxny: n * x < n * y
    by replace int_mult_commute[n, x] | int_mult_commute[n, y]
       xnyn
  apply int_neg_mult_left_cancel_less[n, x, y] to nn, nxny
end

// Left cancellation by a negative Int under `≤` (reverses order).
theorem int_neg_mult_left_cancel_le: all n:Int, x:Int, y:Int.
  if n < +0 and n * x ≤ n * y
  then y ≤ x
proof
  arbitrary n:Int, x:Int, y:Int
  assume prem
  have nn: n < +0 by conjunct 0 of prem
  have nxny: n * x ≤ n * y by conjunct 1 of prem
  have tri: y < x or y = x or x < y by int_trichotomy[y, x]
  cases tri
  case y_l_x: y < x {
    apply int_less_implies_less_equal[y, x] to y_l_x
  }
  case y_eq_x: y = x {
    replace y_eq_x
    int_less_equal_refl[x]
  }
  case x_l_y: x < y {
    have ny_l_nx: n * y < n * x
      by apply int_neg_mult_mono_less_left[n, x, y] to nn, x_l_y
    have bad: n * y < n * y
      by apply int_less_trans_less_equal_right[n * y, n * x, n * y]
         to ny_l_nx, nxny
    conclude false by apply int_less_irreflexive[n * y] to bad
  }
end

// Right cancellation by a negative Int under `≤` (reverses order).
theorem int_neg_mult_right_cancel_le: all n:Int, x:Int, y:Int.
  if n < +0 and x * n ≤ y * n
  then y ≤ x
proof
  arbitrary n:Int, x:Int, y:Int
  assume prem
  have nn: n < +0 by conjunct 0 of prem
  have xnyn: x * n ≤ y * n by conjunct 1 of prem
  have nxny: n * x ≤ n * y
    by replace int_mult_commute[n, x] | int_mult_commute[n, y]
       xnyn
  apply int_neg_mult_left_cancel_le[n, x, y] to nn, nxny
end