module Int

import UInt
import Base

import IntDefs
import IntAddSub
import IntMult
import IntAbs

/*
  Int parity predicates.

  `Even(n)` means `n` is twice another Int, and `Odd(n)` means `n` is
  one plus twice another Int. These overload the corresponding UInt
  predicates from `UIntEvenOdd.pf`; type-directed dispatch picks the
  right one for each call.
*/

fun Even(n : Int) {
  some m:Int. n = +2 * m
}

fun Odd(n : Int) {
  some m:Int. n = +1 + (+2 * m)
}

// Helper: every integer doubled equals itself added to itself.
// Lets the closure proofs avoid the missing Int distributivity laws.
lemma int_two_mult_unfold: all x:Int. +2 * x = x + x
proof
  arbitrary x:Int
  switch x {
    case pos(x') {
      have lhs: +2 * pos(x') = pos(2 * x') by mult_pos_pos[2, x']
      have mid: pos(2 * x') = pos(x' + x') by replace uint_two_mult.
      have rhs: pos(x' + x') = pos(x') + pos(x') by symmetric add_pos_pos[x', x']
      transitive lhs (transitive mid rhs)
    }
    case negsuc(x') {
      have lhs: +2 * negsuc(x') = - pos(2 + 2 * x') by mult_pos_negsuc[2, x']
      have m1: - pos(2 + 2 * x') = negsuc(1 + 2 * x') by neg_pos[1 + 2 * x']
      have m2: negsuc(1 + 2 * x') = negsuc(1 + x' + x') by replace uint_two_mult.
      have rhs: negsuc(1 + x' + x') = negsuc(x') + negsuc(x') by symmetric add_negsuc_negsuc[x', x']
      transitive lhs (transitive m1 (transitive m2 rhs))
    }
  }
end

// Twice any integer is even.
theorem int_two_even: all n:Int. Even(+2 * n)
proof
  arbitrary n:Int
  expand Even
  choose n.
end

// One plus twice any integer is odd.
theorem int_one_two_odd: all n:Int. Odd(+1 + +2 * n)
proof
  arbitrary n:Int
  expand Odd
  choose n.
end

// The sum of two even integers is even.
theorem int_even_add_even: all x:Int, y:Int.
  if Even(x) and Even(y) then Even(x + y)
proof
  arbitrary x:Int, y:Int
  assume prem: Even(x) and Even(y)
  obtain a where x_2a: x = +2 * a from expand Even in (conjunct 0 of prem)
  obtain b where y_2b: y = +2 * b from expand Even in (conjunct 1 of prem)
  expand Even
  choose a + b
  // Goal: x + y = +2 * (a + b)
  // Strategy: rewrite x, y; then +2 * z = z + z; rearrange via commute/assoc.
  have rhs: +2 * (a + b) = (a + b) + (a + b) by int_two_mult_unfold[a + b]
  have lhs: x + y = (a + a) + (b + b) by {
    replace x_2a | y_2b
    replace int_two_mult_unfold.
  }
  // (a + a) + (b + b) = (a + b) + (a + b) by commute/assoc.
  have rearrange: (a + a) + (b + b) = (a + b) + (a + b) by {
    equations
        (a + a) + (b + b)
      = a + (a + (b + b))       by .
    ... = a + ((a + b) + b)     by .
    ... = a + (b + (a + b))     by replace int_add_commute[a + b, b].
    ... = (a + b) + (a + b)     by .
  }
  transitive lhs (transitive rearrange symmetric rhs)
end

// Even + Odd is odd.
theorem int_even_add_odd: all x:Int, y:Int.
  if Even(x) and Odd(y) then Odd(x + y)
proof
  arbitrary x:Int, y:Int
  assume prem: Even(x) and Odd(y)
  obtain a where x_2a: x = +2 * a from expand Even in (conjunct 0 of prem)
  obtain b where y_1_2b: y = +1 + +2 * b from expand Odd in (conjunct 1 of prem)
  expand Odd
  choose a + b
  // Goal: x + y = +1 + +2 * (a + b)
  have rhs: +1 + +2 * (a + b) = +1 + ((a + b) + (a + b))
    by replace int_two_mult_unfold.
  have lhs: x + y = (a + a) + (+1 + (b + b)) by {
    replace x_2a | y_1_2b
    replace int_two_mult_unfold.
  }
  have rearrange: (a + a) + (+1 + (b + b)) = +1 + ((a + b) + (a + b)) by {
    equations
        (a + a) + (+1 + (b + b))
      = a + (a + (+1 + (b + b)))     by .
    ... = a + ((a + +1) + (b + b))   by .
    ... = a + ((+1 + a) + (b + b))   by replace int_add_commute[a, +1].
    ... = a + (+1 + (a + (b + b)))   by .
    ... = (a + +1) + (a + (b + b))   by .
    ... = (+1 + a) + (a + (b + b))   by replace int_add_commute[a, +1].
    ... = +1 + (a + (a + (b + b)))   by .
    ... = +1 + ((a + a) + (b + b))   by .
    ... = +1 + (a + (a + (b + b)))   by .
    ... = +1 + (a + ((a + b) + b))   by .
    ... = +1 + (a + (b + (a + b)))   by replace int_add_commute[a + b, b].
    ... = +1 + ((a + b) + (a + b))   by .
  }
  transitive lhs (transitive rearrange symmetric rhs)
end

// Odd + Even is odd, by commuting.
theorem int_odd_add_even: all x:Int, y:Int.
  if Odd(x) and Even(y) then Odd(x + y)
proof
  arbitrary x:Int, y:Int
  assume prem: Odd(x) and Even(y)
  have odd_yx: Odd(y + x) by {
    apply int_even_add_odd[y, x] to (conjunct 1 of prem), (conjunct 0 of prem)
  }
  replace int_add_commute[x, y]
  odd_yx
end

// Odd + Odd is even.
theorem int_odd_add_odd: all x:Int, y:Int.
  if Odd(x) and Odd(y) then Even(x + y)
proof
  arbitrary x:Int, y:Int
  assume prem: Odd(x) and Odd(y)
  obtain a where x_1_2a: x = +1 + +2 * a from expand Odd in (conjunct 0 of prem)
  obtain b where y_1_2b: y = +1 + +2 * b from expand Odd in (conjunct 1 of prem)
  expand Even
  choose +1 + (a + b)
  // Goal: x + y = +2 * (+1 + (a + b))
  have rhs: +2 * (+1 + (a + b)) = (+1 + (a + b)) + (+1 + (a + b))
    by int_two_mult_unfold[+1 + (a + b)]
  have lhs: x + y = (+1 + (a + a)) + (+1 + (b + b)) by {
    replace x_1_2a | y_1_2b
    replace int_two_mult_unfold.
  }
  have rearrange: (+1 + (a + a)) + (+1 + (b + b))
                = (+1 + (a + b)) + (+1 + (a + b)) by {
    equations
        (+1 + (a + a)) + (+1 + (b + b))
      = +1 + ((a + a) + (+1 + (b + b)))   by .
    ... = +1 + (a + (a + (+1 + (b + b)))) by .
    ... = +1 + (a + ((a + +1) + (b + b))) by .
    ... = +1 + (a + ((+1 + a) + (b + b))) by replace int_add_commute[a, +1].
    ... = +1 + (a + (+1 + (a + (b + b)))) by .
    ... = +1 + ((a + +1) + (a + (b + b))) by .
    ... = +1 + ((+1 + a) + (a + (b + b))) by replace int_add_commute[a, +1].
    ... = +1 + (+1 + (a + (a + (b + b)))) by .
    ... = (+1 + +1) + (a + (a + (b + b))) by .
    ... = (+1 + +1) + (a + ((a + b) + b)) by .
    ... = (+1 + +1) + (a + (b + (a + b))) by replace int_add_commute[a + b, b].
    ... = (+1 + +1) + ((a + b) + (a + b)) by .
    ... = +1 + (+1 + ((a + b) + (a + b))) by .
    ... = (+1 + (+1 + (a + b))) + (a + b) by .
    ... = ((+1 + (a + b)) + +1) + (a + b) by replace int_add_commute[+1, +1 + (a + b)].
    ... = (+1 + (a + b)) + (+1 + (a + b)) by .
  }
  transitive lhs (transitive rearrange symmetric rhs)
end

// If x is even then x * y is even.
theorem int_even_mult_left: all x:Int, y:Int.
  if Even(x) then Even(x * y)
proof
  arbitrary x:Int, y:Int
  assume prem: Even(x)
  obtain a where x_2a: x = +2 * a from expand Even in prem
  expand Even
  choose a * y
  // Goal: x * y = +2 * (a * y)
  equations
      x * y
    = (+2 * a) * y    by replace x_2a.
  ... = +2 * (a * y)  by int_mult_assoc[+2, a, y]
end

// If y is even then x * y is even, by commuting.
theorem int_even_mult_right: all x:Int, y:Int.
  if Even(y) then Even(x * y)
proof
  arbitrary x:Int, y:Int
  assume prem: Even(y)
  have even_yx: Even(y * x) by apply int_even_mult_left[y, x] to prem
  replace int_mult_commute[x, y]
  even_yx
end

// Helper: negation maps Even to Even.
lemma int_even_neg_fwd: all x:Int. if Even(x) then Even(- x)
proof
  arbitrary x:Int
  assume prem
  obtain a where x_2a: x = +2 * a from expand Even in prem
  expand Even
  choose - a
  // Goal: - x = +2 * (- a)
  equations
      - x
    = - (+2 * a)     by replace x_2a.
  ... = - (a * +2)   by replace int_mult_commute[+2, a].
  ... = (- a) * +2   by dist_neg_mult[a, +2]
  ... = +2 * (- a)   by int_mult_commute[- a, +2]
end

// Negation preserves Even parity.
theorem int_even_neg: all x:Int. Even(x) ⇔ Even(- x)
proof
  arbitrary x:Int
  have fwd: if Even(x) then Even(- x) by int_even_neg_fwd[x]
  have bkwd: if Even(- x) then Even(x) by {
    assume prem
    have e: Even(-(- x)) by apply int_even_neg_fwd[- x] to prem
    have eq: -(- x) = x by neg_involutive[x]
    replace eq in e
  }
  fwd, bkwd
end

// Helper: negation maps Odd to Odd.
lemma int_odd_neg_fwd: all x:Int. if Odd(x) then Odd(- x)
proof
  arbitrary x:Int
  assume prem
  obtain a where x_1_2a: x = +1 + +2 * a from expand Odd in prem
  expand Odd
  choose -+1 + (- a)
  // Goal: -x = +1 + +2 * (-+1 + (-a))
  // Compute LHS: -x = -(+1 + +2*a) = -+1 + -(+2*a) = -+1 + +2*(-a)
  have neg_x: - x = -+1 + +2 * (- a) by {
    equations
        - x
      = - (+1 + +2 * a)              by replace x_1_2a.
    ... = (- +1) + - (+2 * a)        by neg_distr_add[+1, +2 * a]
    ... = -+1 + - (a * +2)           by replace int_mult_commute[+2, a].
    ... = -+1 + (- a) * +2           by replace dist_neg_mult[a, +2].
    ... = -+1 + +2 * (- a)           by replace int_mult_commute[- a, +2].
  }
  // Compute RHS via int_two_mult_unfold:
  //   +1 + +2 * (-+1 + (-a)) = +1 + ((-+1 + (-a)) + (-+1 + (-a)))
  have rhs: +1 + +2 * (-+1 + (- a))
          = +1 + ((-+1 + (- a)) + (-+1 + (- a)))
    by replace int_two_mult_unfold.
  // Rearrange the doubled inner sum back to -+1 + +2*(-a):
  //   +1 + ((-+1 + -a) + (-+1 + -a))
  //   = +1 + (-+1 + (-a + (-+1 + -a)))     assoc
  //   = +1 + (-+1 + ((-a + -+1) + -a))     assoc
  //   = +1 + (-+1 + ((-+1 + -a) + -a))     commute -a, -+1
  //   = +1 + (-+1 + (-+1 + (-a + -a)))     assoc
  //   = +1 + ((-+1 + -+1) + (-a + -a))     assoc
  //   = (+1 + (-+1 + -+1)) + (-a + -a)     assoc
  //   = ((+1 + -+1) + -+1) + (-a + -a)     assoc
  //   = (+0 + -+1) + (-a + -a)             int_add_inverse
  //   = -+1 + (-a + -a)                    +0 + n = n
  //   = -+1 + +2 * (-a)                    int_two_mult_unfold
  have rearrange: +1 + ((-+1 + (- a)) + (-+1 + (- a))) = -+1 + +2 * (- a) by {
    have d: (- a) + (- a) = +2 * (- a) by symmetric int_two_mult_unfold[- a]
    equations
        +1 + ((-+1 + (- a)) + (-+1 + (- a)))
      = +1 + (-+1 + ((- a) + (-+1 + (- a))))   by .
    ... = +1 + (-+1 + (((- a) + -+1) + (- a))) by .
    ... = +1 + (-+1 + ((-+1 + (- a)) + (- a))) by replace int_add_commute[- a, -+1].
    ... = +1 + (-+1 + (-+1 + ((- a) + (- a)))) by .
    ... = +1 + ((-+1 + -+1) + ((- a) + (- a))) by .
    ... = (+1 + (-+1 + -+1)) + ((- a) + (- a)) by .
    ... = ((+1 + -+1) + -+1) + ((- a) + (- a)) by .
    ... = (+0 + -+1) + ((- a) + (- a))         by replace int_add_inverse[+1].
    ... = -+1 + ((- a) + (- a))                by .
    ... = -+1 + +2 * (- a)                     by replace d.
  }
  transitive (transitive neg_x (symmetric rearrange)) (symmetric rhs)
end

theorem int_odd_neg: all x:Int. Odd(x) ⇔ Odd(- x)
proof
  arbitrary x:Int
  have fwd: if Odd(x) then Odd(- x) by int_odd_neg_fwd[x]
  have bkwd: if Odd(- x) then Odd(x) by {
    assume prem
    have o: Odd(-(- x)) by apply int_odd_neg_fwd[- x] to prem
    have eq: -(- x) = x by neg_involutive[x]
    replace eq in o
  }
  fwd, bkwd
end

// Bridges: UInt parity lifts to Int parity through `pos`.
lemma int_even_pos: all u:UInt. if Even(u) then Even(pos(u))
proof
  arbitrary u:UInt
  assume prem
  obtain a where ua: u = 2 * a from expand Even in prem
  expand Even
  choose pos(a)
  // Goal: pos(u) = +2 * pos(a)
  equations
      pos(u)
    = pos(2 * a)        by replace ua.
  ... = +2 * pos(a)     by symmetric mult_pos_pos[2, a]
end

lemma int_odd_pos: all u:UInt. if Odd(u) then Odd(pos(u))
proof
  arbitrary u:UInt
  assume prem
  obtain a where ua: u = 1 + 2 * a from expand Odd in prem
  expand Odd
  choose pos(a)
  // Goal: pos(u) = +1 + +2 * pos(a)
  equations
      pos(u)
    = pos(1 + 2 * a)            by replace ua.
  ... = pos(1) + pos(2 * a)     by symmetric add_pos_pos[1, 2 * a]
  ... = +1 + +2 * pos(a)        by replace symmetric mult_pos_pos[2, a].
end

// Every integer is even or odd.
theorem int_Even_or_Odd: all n:Int. Even(n) or Odd(n)
proof
  arbitrary n:Int
  switch n {
    case pos(u) {
      cases uint_Even_or_Odd[u]
      case e {
        have ev: Even(pos(u)) by apply int_even_pos[u] to e
        ev
      }
      case o {
        have od: Odd(pos(u)) by apply int_odd_pos[u] to o
        od
      }
    }
    case negsuc(u) {
      have eq: - pos(1 + u) = negsuc(u) by neg_pos[u]
      cases uint_Even_or_Odd[1 + u]
      case e {
        have ev_pos: Even(pos(1 + u)) by apply int_even_pos[1 + u] to e
        have ev_neg: Even(- pos(1 + u))
          by apply int_even_neg_fwd[pos(1 + u)] to ev_pos
        have ev_ns: Even(negsuc(u)) by replace eq in ev_neg
        ev_ns
      }
      case o {
        have od_pos: Odd(pos(1 + u)) by apply int_odd_pos[1 + u] to o
        have od_neg: Odd(- pos(1 + u))
          by apply int_odd_neg_fwd[pos(1 + u)] to od_pos
        have od_ns: Odd(negsuc(u)) by replace eq in od_neg
        od_ns
      }
    }
  }
end

// Helper: +2 * (- y) = - (+2 * y).
lemma int_two_mult_neg: all y:Int. +2 * (- y) = - (+2 * y)
proof
  arbitrary y:Int
  equations
      +2 * (- y)
    = (- y) * +2     by int_mult_commute[+2, - y]
  ... = - (y * +2)   by symmetric dist_neg_mult[y, +2]
  ... = - (+2 * y)   by replace int_mult_commute[y, +2].
end

// Helper: doubling distributes over Int addition.
lemma int_two_mult_add: all x:Int, y:Int. +2 * x + +2 * y = +2 * (x + y)
proof
  arbitrary x:Int, y:Int
  have rearrange: (x + x) + (y + y) = (x + y) + (x + y) by {
    equations
        (x + x) + (y + y)
      = x + (x + (y + y))     by .
    ... = x + ((x + y) + y)   by .
    ... = x + (y + (x + y))   by replace int_add_commute[x + y, y].
    ... = (x + y) + (x + y)   by .
  }
  equations
      +2 * x + +2 * y
    = (x + x) + (y + y)       by replace int_two_mult_unfold.
  ... = (x + y) + (x + y)     by rearrange
  ... = +2 * (x + y)          by symmetric int_two_mult_unfold[x + y]
end

// Even and not-odd are equivalent for Int.
theorem int_Even_not_Odd: all n:Int. Even(n) ⇔ not Odd(n)
proof
  arbitrary n:Int
  have not_both: not (Even(n) and Odd(n)) by {
    assume both: Even(n) and Odd(n)
    obtain a where na: n = +2 * a from expand Even in (conjunct 0 of both)
    obtain b where nb: n = +1 + +2 * b from expand Odd in (conjunct 1 of both)
    have eq: +2 * a = +1 + +2 * b by transitive (symmetric na) nb
    // From +2 * a = +1 + +2 * b, derive +2 * (a + -b) = +1.
    have rearr: +2 * (a + (- b)) = +1 by {
      equations
          +2 * (a + (- b))
        = +2 * a + +2 * (- b)              by symmetric int_two_mult_add[a, - b]
      ... = +2 * a + (- (+2 * b))          by replace int_two_mult_neg[b].
      ... = (+1 + +2 * b) + (- (+2 * b))   by replace eq.
      ... = +1 + (+2 * b + (- (+2 * b)))   by int_add_assoc[+1, +2 * b, - (+2 * b)]
      ... = +1 + +0                        by replace int_add_inverse[+2 * b].
      ... = +1                             by .
    }
    // Taking abs of both sides yields 1 = 2 * abs(a + -b), so 1 is UInt-Even.
    have one_eq_two_abs: 1 = 2 * abs(a + (- b)) by {
      have h: abs(+2 * (a + (- b))) = 2 * abs(a + (- b))
        by int_abs_mult[+2, a + (- b)]
      replace rearr in h
    }
    have one_even: Even(1) by {
      expand Even
      choose abs(a + (- b))
      one_eq_two_abs
    }
    have one_odd: Odd(1) by {
      expand Odd
      choose 0
      .
    }
    have not_odd: not Odd(1)
      by apply (conjunct 0 of uint_Even_not_Odd[1]) to one_even
    apply not_odd to one_odd
  }
  have fwd: if Even(n) then not Odd(n) by {
    assume e
    assume o
    have both: Even(n) and Odd(n) by e, o
    apply not_both to both
  }
  have bkwd: if not Odd(n) then Even(n) by {
    assume not_o
    cases int_Even_or_Odd[n]
    case e { e }
    case o { conclude false by apply not_o to o }
  }
  fwd, bkwd
end

// Subtracting one from an odd successor leaves an even number.
theorem int_odd_one_even: all n:Int. if Odd(+1 + n) then Even(n)
proof
  arbitrary n:Int
  assume prem: Odd(+1 + n)
  cases int_Even_or_Odd[n]
  case e_n { e_n }
  case o_n {
    have odd_one: Odd(+1) by {
      expand Odd
      choose +0
      .
    }
    have ev_1n: Even(+1 + n) by apply int_odd_add_odd[+1, n] to odd_one, o_n
    have not_odd: not Odd(+1 + n)
      by apply (conjunct 0 of int_Even_not_Odd[+1 + n]) to ev_1n
    conclude false by apply not_odd to prem
  }
end

// Subtracting one from an even successor leaves an odd number.
theorem int_even_one_odd: all n:Int. if Even(+1 + n) then Odd(n)
proof
  arbitrary n:Int
  assume prem: Even(+1 + n)
  cases int_Even_or_Odd[n]
  case e_n {
    have odd_one: Odd(+1) by {
      expand Odd
      choose +0
      .
    }
    have odd_1n: Odd(+1 + n) by apply int_odd_add_even[+1, n] to odd_one, e_n
    have not_odd: not Odd(+1 + n)
      by apply (conjunct 0 of int_Even_not_Odd[+1 + n]) to prem
    conclude false by apply not_odd to odd_1n
  }
  case o_n { o_n }
end

// Odd × Odd is odd.
theorem int_odd_mult_odd: all x:Int, y:Int.
  if Odd(x) and Odd(y) then Odd(x * y)
proof
  arbitrary x:Int, y:Int
  assume prem: Odd(x) and Odd(y)
  obtain a where x_1_2a: x = +1 + +2 * a from expand Odd in (conjunct 0 of prem)
  obtain b where y_1_2b: y = +1 + +2 * b from expand Odd in (conjunct 1 of prem)
  expand Odd
  choose b + a * (+1 + +2 * b)
  equations
      x * y
    = (+1 + +2 * a) * y                                  by replace x_1_2a.
... = +1 * y + (+2 * a) * y                              by int_dist_mult_add_right[y, +1, +2 * a]
... = y + (+2 * a) * y                                   by .
... = (+1 + +2 * b) + (+2 * a) * (+1 + +2 * b)           by replace y_1_2b.
... = +1 + (+2 * b + (+2 * a) * (+1 + +2 * b))           by .
... = +1 + (+2 * b + +2 * (a * (+1 + +2 * b)))           by .
... = +1 + #+2 * (b + a * (+1 + +2 * b))#                by replace int_dist_mult_add[+2, b, a * (+1 + +2 * b)].
end

// Parity via `abs`: an Int is Even iff its absolute value is UInt-Even.
// Forward uses the multiplicative form of abs on `x = +2 * m`; backward
// splits on `x`, reusing `int_even_pos` for the `pos` case and combining
// it with `int_even_neg_fwd` and `neg_pos` for the `negsuc` case.
theorem int_Even_iff_abs_Even: all x:Int. Even(x) ⇔ Even(abs(x))
proof
  arbitrary x:Int
  have fwd: if Even(x) then Even(abs(x)) by {
    assume prem
    obtain m where eq: x = +2 * m from expand Even in prem
    expand Even
    choose abs(m)
    equations
        abs(x)
      = abs(+2 * m)         by replace eq.
    ... = abs(+2) * abs(m)  by int_abs_mult[+2, m]
    ... = 2 * abs(m)        by .
  }
  have bkwd: if Even(abs(x)) then Even(x) by {
    switch x {
      case pos(u) {
        assume prem
        apply int_even_pos[u] to prem
      }
      case negsuc(u) {
        assume prem
        have ev_pos: Even(pos(1 + u))
          by apply int_even_pos[1 + u] to prem
        have ev_neg: Even(- pos(1 + u))
          by apply int_even_neg_fwd[pos(1 + u)] to ev_pos
        have eq: - pos(1 + u) = negsuc(u) by neg_pos[u]
        replace eq in ev_neg
      }
    }
  }
  fwd, bkwd
end

// Parity via `abs`: an Int is Odd iff its absolute value is UInt-Odd.
// `abs` doesn't distribute over addition, so we route through the
// Even-not-Odd equivalences (`int_Even_not_Odd` and `uint_Even_not_Odd`)
// and the Even/abs bridge established above.
theorem int_Odd_iff_abs_Odd: all x:Int. Odd(x) ⇔ Odd(abs(x))
proof
  arbitrary x:Int
  have iEi: Even(x) ⇔ not Odd(x) by int_Even_not_Odd[x]
  have uEi: Even(abs(x)) ⇔ not Odd(abs(x)) by uint_Even_not_Odd[abs(x)]
  have abs_iff: Even(x) ⇔ Even(abs(x)) by int_Even_iff_abs_Even[x]
  have fwd: if Odd(x) then Odd(abs(x)) by {
    assume o_x
    cases uint_Even_or_Odd[abs(x)]
    case e_abs {
      have e_x: Even(x) by apply (conjunct 1 of abs_iff) to e_abs
      have not_o: not Odd(x) by apply (conjunct 0 of iEi) to e_x
      conclude false by apply not_o to o_x
    }
    case o_abs {
      o_abs
    }
  }
  have bkwd: if Odd(abs(x)) then Odd(x) by {
    assume o_abs
    cases int_Even_or_Odd[x]
    case e_x {
      have e_abs: Even(abs(x)) by apply (conjunct 0 of abs_iff) to e_x
      have not_o: not Odd(abs(x)) by apply (conjunct 0 of uEi) to e_abs
      conclude false by apply not_o to o_abs
    }
    case o_x {
      o_x
    }
  }
  fwd, bkwd
end