no goals
m n k : Nat
⊢ -[m+1] * subNatNat n k = subNatNat (succ m * k) (succ m * n)
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)
  rw [subNatNat_of_lt h, subNatNat_of_le (Nat.le_of_lt h')]
  simp [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h), Nat.mul_sub_left_distrib]
| inr h => cases Nat.lt_or_ge k n with
  | inl h' =>
    have h₁ : succ m * n > succ m * k := Nat.mul_lt_mul_of_pos_left h' (Nat.succ_pos m)
    rw [subNatNat_of_le h, subNatNat_of_lt h₁, negSucc_mul_ofNat,
      Nat.mul_sub_left_distrib, ← succ_pred_eq_of_pos (Nat.sub_pos_of_lt h₁)]; rfl
  | inr h' => rw [Nat.le_antisymm h h', subNatNat_self, subNatNat_self, Int.mul_zero]
case inl
m n k : Nat
h : n < k
h' : succ m * n < succ m * k
⊢ -[m+1] * subNatNat n k = subNatNat (succ m * k) (succ m * n)
case inl
m n k : Nat
h : n < k
⊢ -[m+1] * subNatNat n k = subNatNat (succ m * k) (succ m * n)
have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m)
case inl
m n k : Nat
h : n < k
h' : succ m * n < succ m * k
⊢ -[m+1] * -[pred (k - n)+1] = ↑(succ m * k - succ m * n)
case inl
m n k : Nat
h : n < k
h' : succ m * n < succ m * k
⊢ -[m+1] * subNatNat n k = subNatNat (succ m * k) (succ m * n)
rw [subNatNat_of_lt h, subNatNat_of_le (Nat.le_of_lt h')]
no goals
case inl
m n k : Nat
h : n < k
h' : succ m * n < succ m * k
⊢ -[m+1] * -[pred (k - n)+1] = ↑(succ m * k - succ m * n)
simp [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h), Nat.mul_sub_left_distrib]
no goals
case inr
m n k : Nat
h : n ≥ k
⊢ -[m+1] * subNatNat n k = subNatNat (succ m * k) (succ m * n)
cases Nat.lt_or_ge k n with
| inl h' =>
have h₁ : succ m * n > succ m * k := Nat.mul_lt_mul_of_pos_left h' (Nat.succ_pos m)
rw [subNatNat_of_le h, subNatNat_of_lt h₁, negSucc_mul_ofNat,
Nat.mul_sub_left_distrib, ← succ_pred_eq_of_pos (Nat.sub_pos_of_lt h₁)]; rfl
| inr h' => rw [Nat.le_antisymm h h', subNatNat_self, subNatNat_self, Int.mul_zero]
case inr.inl
m n k : Nat
h : n ≥ k
h' : k < n
h₁ : succ m * n > succ m * k
⊢ -[m+1] * subNatNat n k = subNatNat (succ m * k) (succ m * n)
case inr.inl
m n k : Nat
h : n ≥ k
h' : k < n
⊢ -[m+1] * subNatNat n k = subNatNat (succ m * k) (succ m * n)
have h₁ : succ m * n > succ m * k := Nat.mul_lt_mul_of_pos_left h' (Nat.succ_pos m)
case inr.inl
m n k : Nat
h : n ≥ k
h' : k < n
h₁ : succ m * n > succ m * k
⊢ -↑(succ (pred (succ m * n - succ m * k))) = -[pred (succ (pred (succ m * n - succ m * k)))+1]
case inr.inl
m n k : Nat
h : n ≥ k
h' : k < n
h₁ : succ m * n > succ m * k
⊢ -[m+1] * subNatNat n k = subNatNat (succ m * k) (succ m * n)
rw [subNatNat_of_le h, subNatNat_of_lt h₁, negSucc_mul_ofNat,
  Nat.mul_sub_left_distrib, ← succ_pred_eq_of_pos (Nat.sub_pos_of_lt h₁)]
no goals
case inr.inl
m n k : Nat
h : n ≥ k
h' : k < n
h₁ : succ m * n > succ m * k
⊢ -↑(succ (pred (succ m * n - succ m * k))) = -[pred (succ (pred (succ m * n - succ m * k)))+1]
rfl
no goals
case inr.inr
m n k : Nat
h : n ≥ k
h' : k ≥ n
⊢ -[m+1] * subNatNat n k = subNatNat (succ m * k) (succ m * n)
rw [Nat.le_antisymm h h', subNatNat_self, subNatNat_self, Int.mul_zero]