-- Multiplication and the order of the integers: signs of products,
-- cancellation, and squares
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Int.OrderMul
import Order

theorem integerLe.mul_nonneg (x y : Integer)
  requires first : 0 ≤ x
  requires second : 0 ≤ y
  shows 0 ≤ x * y
proof
  have xNonnegative := integerLe.zero_iff.forward with first
  have yNonnegative := integerLe.zero_iff.forward with second
  apply integerLe.zero_iff.backward
  exact IntegerNonnegative.mul with xNonnegative, yNonnegative

theorem integerLess.mul_positive (x y : Integer)
  requires first : 0 < x
  requires second : 0 < y
  shows 0 < x * y
proof
  have xPositive := integerLess.zero_iff_positive.forward with first
  have yPositive := integerLess.zero_iff_positive.forward with second
  apply integerLess.zero_iff_positive.backward
  exact IntegerPositive.mul with xPositive, yPositive

theorem integerLe.mul_left (x y k : Integer)
  requires nonnegative : 0 ≤ k
  requires below : x ≤ y
  shows k * x ≤ k * y
proof
  have difference := integerLe.sub_nonneg_iff.forward with below
  have product := integerLe.mul_nonneg with nonnegative, difference
  have shape : k * y - k * x = k * (y - x) by ring
  apply integerLe.sub_nonneg_iff.backward
  rw shape
  exact product

theorem integerLe.mul_right (x y k : Integer)
  requires nonnegative : 0 ≤ k
  requires below : x ≤ y
  shows x * k ≤ y * k
proof
  have scaled := integerLe.mul_left with nonnegative, below
  have left : k * x = x * k by ring
  have right : k * y = y * k by ring
  rw [left, right] at scaled
  exact scaled

theorem integerLess.mul_left (x y k : Integer)
  requires positive : 0 < k
  requires below : x < y
  shows k * x < k * y
proof
  have difference := integerLess.sub_positive_iff.forward with below
  have product := integerLess.mul_positive with positive, difference
  have shape : k * y - k * x = k * (y - x) by ring
  apply integerLess.sub_positive_iff.backward
  rw shape
  exact product

theorem integerLess.mul_right (x y k : Integer)
  requires positive : 0 < k
  requires below : x < y
  shows x * k < y * k
proof
  have scaled := integerLess.mul_left with positive, below
  have left : k * x = x * k by ring
  have right : k * y = y * k by ring
  rw [left, right] at scaled
  exact scaled

theorem integerLe.mul (a b c d : Integer)
  requires aNonnegative : 0 ≤ a
  requires first : a ≤ b
  requires cNonnegative : 0 ≤ c
  requires second : c ≤ d
  shows a * c ≤ b * d
proof
  have dNonnegative := integerLe.transitive with cNonnegative, second
  have left := integerLe.mul_left at c, d, a with aNonnegative, second
  have right := integerLe.mul_right at a, b, d with dNonnegative, first
  exact integerLe.transitive with left, right

theorem integerLe.mul_nonpos (x y : Integer)
  requires nonpositive : x ≤ 0
  requires nonnegative : 0 ≤ y
  shows x * y ≤ 0
proof
  have negated := integerLe.neg_nonneg_iff.backward with nonpositive
  have product := integerLe.mul_nonneg with negated, nonnegative
  have shape : (-x) * y = -(x * y) by ring
  rw shape at product
  exact integerLe.neg_nonneg_iff.forward with product

theorem integerLe.mul_nonpos_right (x y : Integer)
  requires nonnegative : 0 ≤ x
  requires nonpositive : y ≤ 0
  shows x * y ≤ 0
proof
  have swapped := integerLe.mul_nonpos with nonpositive, nonnegative
  have shape : y * x = x * y by ring
  rw shape at swapped
  exact swapped

theorem integerLe.mul_nonpos_nonpos (x y : Integer)
  requires first : x ≤ 0
  requires second : y ≤ 0
  shows 0 ≤ x * y
proof
  have xNegated := integerLe.neg_nonneg_iff.backward with first
  have yNegated := integerLe.neg_nonneg_iff.backward with second
  have product := integerLe.mul_nonneg with xNegated, yNegated
  have shape : (-x) * (-y) = x * y by ring
  rw shape at product
  exact product

theorem integerLess.mul_negative (x y : Integer)
  requires positive : 0 < x
  requires negative : y < 0
  shows x * y < 0
proof
  have negated := integerLess.neg.forward with negative
  have zero : -integerZero = 0
    ring
  rw zero at negated
  have product := integerLess.mul_positive with positive, negated
  have shape : x * (-y) = -(x * y) by ring
  rw shape at product
  have flipped := integerLess.neg at x * y, integerZero
  rw zero at flipped
  exact flipped.backward with product

theorem integerLess.mul_negative_negative (x y : Integer)
  requires first : x < 0
  requires second : y < 0
  shows 0 < x * y
proof
  have zero : -integerZero = 0 by ring
  have xNegated := integerLess.neg.forward with first
  have yNegated := integerLess.neg.forward with second
  rw zero at xNegated
  rw zero at yNegated
  have product := integerLess.mul_positive with xNegated, yNegated
  have shape : (-x) * (-y) = x * y by ring
  rw shape at product
  exact product

theorem integerLe.square_nonneg (x : Integer)
  shows 0 ≤ x * x
proof
  have split := integerLe.cases_sign at x
  cases split with nonnegative | nonpositive
  . exact integerLe.mul_nonneg with nonnegative, nonnegative
  . exact integerLe.mul_nonpos_nonpos with nonpositive, nonpositive

theorem integerMulValue.eq_zero (x y : Integer)
  requires zero : x * y = 0
  shows x = 0 ∨ y = 0
proof
  have xNat := integerNatAbs.natural at x
  have yNat := integerNatAbs.natural at y
  have magnitudes := integerNatAbs.mul at x, y
  rw zero at magnitudes
  have vanish := integerNatAbs.zero
  rw vanish at magnitudes
  symm at magnitudes
  have split := mul.eq_zero_iff.forward with magnitudes
  cases split with xZero | yZero
  . left
    exact integerNatAbs.zero_iff.forward with xZero
  . right
    exact integerNatAbs.zero_iff.forward with yZero

theorem integerMulValue.eq_zero_iff (x y : Integer)
  shows x * y = 0 ↔ x = 0 ∨ y = 0
proof
  constructor
  . intro zero
    exact integerMulValue.eq_zero with zero
  . intro split
    cases split with xZero | yZero
    . rw xZero
      ring
    . rw yZero
      ring

theorem integerMulValue.nonzero (x y : Integer)
  requires first : x ≠ 0
  requires second : y ≠ 0
  shows x * y ≠ 0
proof
  intro zero
  have split := integerMulValue.eq_zero with zero
  cases split with xZero | yZero
  . exact first with xZero
  . exact second with yZero

theorem integerMulValue.square_eq_zero (x : Integer)
  requires zero : x * x = 0
  shows x = 0
proof
  have split := integerMulValue.eq_zero with zero
  cases split with first | second
  . exact first
  . exact second

theorem integerMulValue.square_eq_zero_iff (x : Integer)
  shows x * x = 0 ↔ x = 0
proof
  constructor
  . intro zero
    exact integerMulValue.square_eq_zero with zero
  . intro zero
    rw zero
    ring

theorem integerLess.square_positive (x : Integer)
  requires nonzero : x ≠ 0
  shows 0 < x * x
proof
  have nonnegative := integerLe.square_nonneg at x
  have distinct : 0 ≠ x * x
    intro zero
    symm at zero
    have same := integerMulValue.square_eq_zero with zero
    exact nonzero with same
  exact integerLess.of_le_ne with nonnegative, distinct

theorem integerMulValue.left_cancel (x y k : Integer)
  requires nonzero : k ≠ 0
  requires same : k * x = k * y
  shows x = y
proof
  have product : k * (x - y) = 0
    have shape : k * (x - y) = k * x - k * y by ring
    rw [shape, same]
    ring
  have split := integerMulValue.eq_zero with product
  cases split with kZero | difference
  . exfalso
    exact nonzero with kZero
  . linear_combination difference

theorem integerMulValue.right_cancel (x y k : Integer)
  requires nonzero : k ≠ 0
  requires same : x * k = y * k
  shows x = y
proof
  have left : x * k = k * x by ring
  have right : y * k = k * y by ring
  rw [left, right] at same
  exact integerMulValue.left_cancel with nonzero, same

theorem integerLe.mul_left_cancel (x y k : Integer)
  requires positive : 0 < k
  requires below : k * x ≤ k * y
  shows x ≤ y
proof
  apply integerLe.of_not_less
  intro above
  have scaled := integerLess.mul_left at y, x, k with positive, above
  exact integerLe.not_less with below, scaled

theorem integerLe.mul_right_cancel (x y k : Integer)
  requires positive : 0 < k
  requires below : x * k ≤ y * k
  shows x ≤ y
proof
  have left : x * k = k * x by ring
  have right : y * k = k * y by ring
  rw [left, right] at below
  exact integerLe.mul_left_cancel with positive, below

theorem integerLess.mul_left_cancel (x y k : Integer)
  requires positive : 0 < k
  requires below : k * x < k * y
  shows x < y
proof
  apply integerLess.of_not_le
  intro above
  have weak := integerLess.implies_le with positive
  have scaled := integerLe.mul_left at y, x, k with weak, above
  exact integerLess.not_le with below, scaled

theorem integerLess.mul_right_cancel (x y k : Integer)
  requires positive : 0 < k
  requires below : x * k < y * k
  shows x < y
proof
  have left : x * k = k * x by ring
  have right : y * k = k * y by ring
  rw [left, right] at below
  exact integerLess.mul_left_cancel with positive, below

theorem integerLe.sum_squares_eq_zero (x y : Integer)
  requires zero : x * x + y * y = 0
  shows x = 0 ∧ y = 0
proof
  have xSquare := integerLe.square_nonneg at x
  have ySquare := integerLe.square_nonneg at y
  have xZero : x * x = 0
    have upper : x * x ≤ 0
      have shape : x * x = 0 - y * y by linear_combination zero
      rw shape
      have flipped := integerLe.neg_nonneg_iff.forward at y * y
      have negShape : -(y * y) = 0 - y * y by ring
      rw negShape at flipped
      have negated := integerLe.neg.forward with ySquare
      have zeroNeg : -integerZero = 0 by ring
      rw [zeroNeg, negShape] at negated
      exact negated
    exact integerLe.antisymmetric with upper, xSquare
  have yZero : y * y = 0 by linear_combination zero - xZero
  constructor
  . exact integerMulValue.square_eq_zero with xZero
  . exact integerMulValue.square_eq_zero with yZero

theorem integerLe.le_square (x : Integer)
  shows x ≤ x * x
proof
  have split := integerLe.cases_sign at x
  cases split with nonnegative | nonpositive
  . have cases := integerLe.cases with nonnegative
    cases cases with positive | zero
    . have one := integerLess.one_le_of_positive with positive
      have scaled :=
        integerLe.mul_left at integerOne, x, x with nonnegative, one
      have unit : x * 1 = x by ring
      rw unit at scaled
      exact scaled
    . rw ← zero
      have vanish : integerZero * 0 = 0 by ring
      rw vanish
      exact integerLe.reflexive with *
  . have square := integerLe.square_nonneg at x
    exact integerLe.transitive with nonpositive, square

theorem integerLess.of_one_le (x : Integer)
  requires one : 1 ≤ x
  shows 0 < x
proof
  unfold integerLess
  have shape : integerZero + 1 = integerOne by ring
  rw shape
  exact one

theorem integerLess.positive_iff_one_le (x : Integer)
  shows 0 < x ↔ 1 ≤ x
proof
  constructor
  . intro positive
    exact integerLess.one_le_of_positive with positive
  . intro one
    exact integerLess.of_one_le with one