no goals
z x y : Nat
y0 : y = 0
⊢ z * x % (z * y) = z * (x % y)
rw [y0, Nat.mul_zero, mod_zero, mod_zero]
no goals
z x y : Nat
y0 : ¬y = 0
z0 : z = 0
⊢ z * x % (z * y) = z * (x % y)
rw [z0, Nat.zero_mul, Nat.zero_mul, Nat.zero_mul, mod_zero]
no goals
z x y : Nat
y0 : ¬y = 0
z0 : ¬z = 0
⊢ z * x % (z * y) = z * (x % y)
induction x using Nat.strongInductionOn with
| _ n IH =>
  have y0 : y > 0 := Nat.pos_of_ne_zero y0
  have z0 : z > 0 := Nat.pos_of_ne_zero z0
  cases Nat.lt_or_ge n y with
  | inl yn => rw [mod_eq_of_lt yn, mod_eq_of_lt (Nat.mul_lt_mul_of_pos_left yn z0)]
  | inr yn =>
    rw [mod_eq_sub_mod yn, mod_eq_sub_mod (Nat.mul_le_mul_left z yn),
      ← Nat.mul_sub_left_distrib]
    exact IH _ (sub_lt (Nat.lt_of_lt_of_le y0 yn) y0)
case ind
z y : Nat
y0✝ : ¬y = 0
z0 : ¬z = 0
n : Nat
IH : ∀ (m : Nat), m < n → z * m % (z * y) = z * (m % y)
y0 : y > 0
⊢ z * n % (z * y) = z * (n % y)
case ind
z y : Nat
y0 : ¬y = 0
z0 : ¬z = 0
n : Nat
IH : ∀ (m : Nat), m < n → z * m % (z * y) = z * (m % y)
⊢ z * n % (z * y) = z * (n % y)
have y0 : y > 0 := Nat.pos_of_ne_zero y0
case ind
z y : Nat
y0✝ : ¬y = 0
z0✝ : ¬z = 0
n : Nat
IH : ∀ (m : Nat), m < n → z * m % (z * y) = z * (m % y)
y0 : y > 0
z0 : z > 0
⊢ z * n % (z * y) = z * (n % y)
case ind
z y : Nat
y0✝ : ¬y = 0
z0 : ¬z = 0
n : Nat
IH : ∀ (m : Nat), m < n → z * m % (z * y) = z * (m % y)
y0 : y > 0
⊢ z * n % (z * y) = z * (n % y)
have z0 : z > 0 := Nat.pos_of_ne_zero z0
no goals
case ind
z y : Nat
y0✝ : ¬y = 0
z0✝ : ¬z = 0
n : Nat
IH : ∀ (m : Nat), m < n → z * m % (z * y) = z * (m % y)
y0 : y > 0
z0 : z > 0
⊢ z * n % (z * y) = z * (n % y)
cases Nat.lt_or_ge n y with
| inl yn => rw [mod_eq_of_lt yn, mod_eq_of_lt (Nat.mul_lt_mul_of_pos_left yn z0)]
| inr yn =>
  rw [mod_eq_sub_mod yn, mod_eq_sub_mod (Nat.mul_le_mul_left z yn),
    ← Nat.mul_sub_left_distrib]
  exact IH _ (sub_lt (Nat.lt_of_lt_of_le y0 yn) y0)
no goals
case ind.inl
z y : Nat
y0✝ : ¬y = 0
z0✝ : ¬z = 0
n : Nat
IH : ∀ (m : Nat), m < n → z * m % (z * y) = z * (m % y)
y0 : y > 0
z0 : z > 0
yn : n < y
⊢ z * n % (z * y) = z * (n % y)
rw [mod_eq_of_lt yn, mod_eq_of_lt (Nat.mul_lt_mul_of_pos_left yn z0)]
case ind.inr
z y : Nat
y0✝ : ¬y = 0
z0✝ : ¬z = 0
n : Nat
IH : ∀ (m : Nat), m < n → z * m % (z * y) = z * (m % y)
y0 : y > 0
z0 : z > 0
yn : n ≥ y
⊢ z * (n - y) % (z * y) = z * ((n - y) % y)
case ind.inr
z y : Nat
y0✝ : ¬y = 0
z0✝ : ¬z = 0
n : Nat
IH : ∀ (m : Nat), m < n → z * m % (z * y) = z * (m % y)
y0 : y > 0
z0 : z > 0
yn : n ≥ y
⊢ z * n % (z * y) = z * (n % y)
rw [mod_eq_sub_mod yn, mod_eq_sub_mod (Nat.mul_le_mul_left z yn),
  ← Nat.mul_sub_left_distrib]
no goals
case ind.inr
z y : Nat
y0✝ : ¬y = 0
z0✝ : ¬z = 0
n : Nat
IH : ∀ (m : Nat), m < n → z * m % (z * y) = z * (m % y)
y0 : y > 0
z0 : z > 0
yn : n ≥ y
⊢ z * (n - y) % (z * y) = z * ((n - y) % y)
exact IH _ (sub_lt (Nat.lt_of_lt_of_le y0 yn) y0)