no goals
m n k : Nat
⊢ ↑m * subNatNat n k = subNatNat (m * n) (m * k)
cases m with
| zero => simp [ofNat_zero, Int.zero_mul, Nat.zero_mul]
| succ m => cases n.lt_or_ge k with
  | inl h =>
    have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m)
    simp [subNatNat_of_lt h, subNatNat_of_lt h']
    rw [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h), ← neg_ofNat_succ, Nat.mul_sub_left_distrib,
      ← succ_pred_eq_of_pos (Nat.sub_pos_of_lt h')]; rfl
  | inr h =>
    have h' : succ m * k ≤ succ m * n := Nat.mul_le_mul_left _ h
    simp [subNatNat_of_le h, subNatNat_of_le h', Nat.mul_sub_left_distrib]
no goals
case zero
n k : Nat
⊢ ↑zero * subNatNat n k = subNatNat (zero * n) (zero * k)
simp [ofNat_zero, Int.zero_mul, Nat.zero_mul]
no goals
case succ
n k m : Nat
⊢ ↑(succ m) * subNatNat n k = subNatNat (succ m * n) (succ m * k)
cases n.lt_or_ge k with
| inl h =>
have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m)
simp [subNatNat_of_lt h, subNatNat_of_lt h']
rw [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h), ← neg_ofNat_succ, Nat.mul_sub_left_distrib,
← succ_pred_eq_of_pos (Nat.sub_pos_of_lt h')]; rfl
| inr h =>
have h' : succ m * k ≤ succ m * n := Nat.mul_le_mul_left _ h
simp [subNatNat_of_le h, subNatNat_of_le h', Nat.mul_sub_left_distrib]
case succ.inl
n k m : Nat
h : n < k
h' : succ m * n < succ m * k
⊢ ↑(succ m) * subNatNat n k = subNatNat (succ m * n) (succ m * k)
case succ.inl
n k m : Nat
h : n < k
⊢ ↑(succ m) * subNatNat n k = subNatNat (succ m * n) (succ m * k)
have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m)
case succ.inl
n k m : Nat
h : n < k
h' : succ m * n < succ m * k
⊢ negOfNat (succ m * succ (pred (k - n))) = -[pred (succ m * k - succ m * n)+1]
case succ.inl
n k m : Nat
h : n < k
h' : succ m * n < succ m * k
⊢ ↑(succ m) * subNatNat n k = subNatNat (succ m * n) (succ m * k)
simp [subNatNat_of_lt h, subNatNat_of_lt h']
case succ.inl
n k m : Nat
h : n < k
h' : succ m * n < succ m * k
⊢ negOfNat (succ (pred (succ m * k - succ m * n))) = -↑(succ (pred (succ (pred (succ m * k - succ m * n)))))
case succ.inl
n k m : Nat
h : n < k
h' : succ m * n < succ m * k
⊢ negOfNat (succ m * succ (pred (k - n))) = -[pred (succ m * k - succ m * n)+1]
rw [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h), ← neg_ofNat_succ, Nat.mul_sub_left_distrib,
  ← succ_pred_eq_of_pos (Nat.sub_pos_of_lt h')]
no goals
case succ.inl
n k m : Nat
h : n < k
h' : succ m * n < succ m * k
⊢ negOfNat (succ (pred (succ m * k - succ m * n))) = -↑(succ (pred (succ (pred (succ m * k - succ m * n)))))
rfl
case succ.inr
n k m : Nat
h : n ≥ k
h' : succ m * k ≤ succ m * n
⊢ ↑(succ m) * subNatNat n k = subNatNat (succ m * n) (succ m * k)
case succ.inr
n k m : Nat
h : n ≥ k
⊢ ↑(succ m) * subNatNat n k = subNatNat (succ m * n) (succ m * k)
have h' : succ m * k ≤ succ m * n := Nat.mul_le_mul_left _ h
no goals
case succ.inr
n k m : Nat
h : n ≥ k
h' : succ m * k ≤ succ m * n
⊢ ↑(succ m) * subNatNat n k = subNatNat (succ m * n) (succ m * k)
simp [subNatNat_of_le h, subNatNat_of_le h', Nat.mul_sub_left_distrib]