no goals
m n k : Nat
⊢ ↑m * (↑n + ↑k) = ↑m * ↑n + ↑m * ↑k
simp [Nat.left_distrib]
m n k : Nat
⊢ subNatNat (m * n) (m * succ k) = ↑(m * n) + subNatNat 0 (m * succ k)
m n k : Nat
⊢ ↑m * (↑n + -[k+1]) = ↑m * ↑n + ↑m * -[k+1]
simp [negOfNat_eq_subNatNat_zero]
m n k : Nat
⊢ subNatNat (m * n) (m * succ k) = subNatNat (m * n + 0) (m * succ k)
m n k : Nat
⊢ subNatNat (m * n) (m * succ k) = ↑(m * n) + subNatNat 0 (m * succ k)
rw [← subNatNat_add]
no goals
m n k : Nat
⊢ subNatNat (m * n) (m * succ k) = subNatNat (m * n + 0) (m * succ k)
rfl
m n k : Nat
⊢ subNatNat (m * k) (m * succ n) = subNatNat 0 (m * succ n) + ↑(m * k)
m n k : Nat
⊢ ↑m * (-[n+1] + ↑k) = ↑m * -[n+1] + ↑m * ↑k
simp [negOfNat_eq_subNatNat_zero]
m n k : Nat
⊢ subNatNat (m * k) (m * succ n) = subNatNat (m * k + 0) (m * succ n)
m n k : Nat
⊢ subNatNat (m * k) (m * succ n) = subNatNat 0 (m * succ n) + ↑(m * k)
rw [Int.add_comm, ← subNatNat_add]
no goals
m n k : Nat
⊢ subNatNat (m * k) (m * succ n) = subNatNat (m * k + 0) (m * succ n)
rfl
m n k : Nat
⊢ negOfNat (m * succ (succ (n + k))) = negOfNat (m * succ n + m * succ k)
m n k : Nat
⊢ ↑m * (-[n+1] + -[k+1]) = ↑m * -[n+1] + ↑m * -[k+1]
simp
m n k : Nat
⊢ negOfNat (m * succ (succ (n + k))) = negOfNat (m * succ (n + succ k))
m n k : Nat
⊢ negOfNat (m * succ (succ (n + k))) = negOfNat (m * succ n + m * succ k)
rw [← Nat.left_distrib, succ_add]
no goals
m n k : Nat
⊢ negOfNat (m * succ (succ (n + k))) = negOfNat (m * succ (n + succ k))
rfl
m n k : Nat
⊢ negOfNat ((n + k) * succ m) = negOfNat (n * succ m + k * succ m)
m n k : Nat
⊢ -[m+1] * (↑n + ↑k) = -[m+1] * ↑n + -[m+1] * ↑k
simp [Nat.mul_comm]
no goals
m n k : Nat
⊢ negOfNat ((n + k) * succ m) = negOfNat (n * succ m + k * succ m)
rw [← Nat.right_distrib, Nat.mul_comm]
m n k : Nat
⊢ subNatNat (succ m * succ k) (succ m * n) = subNatNat 0 (succ m * n) + ↑(succ m * succ k)
m n k : Nat
⊢ -[m+1] * (↑n + -[k+1]) = -[m+1] * ↑n + -[m+1] * -[k+1]
simp [negOfNat_eq_subNatNat_zero]
m n k : Nat
⊢ subNatNat (succ m * succ k) (succ m * n) = subNatNat (succ m * succ k + 0) (succ m * n)
m n k : Nat
⊢ subNatNat (succ m * succ k) (succ m * n) = subNatNat 0 (succ m * n) + ↑(succ m * succ k)
rw [Int.add_comm, ← subNatNat_add]
no goals
m n k : Nat
⊢ subNatNat (succ m * succ k) (succ m * n) = subNatNat (succ m * succ k + 0) (succ m * n)
rfl
m n k : Nat
⊢ subNatNat (succ m * succ n) (succ m * k) = ↑(succ m * succ n) + subNatNat 0 (succ m * k)
m n k : Nat
⊢ -[m+1] * (-[n+1] + ↑k) = -[m+1] * -[n+1] + -[m+1] * ↑k
simp [negOfNat_eq_subNatNat_zero]
m n k : Nat
⊢ subNatNat (succ m * succ n) (succ m * k) = subNatNat (succ m * succ n + 0) (succ m * k)
m n k : Nat
⊢ subNatNat (succ m * succ n) (succ m * k) = ↑(succ m * succ n) + subNatNat 0 (succ m * k)
rw [← subNatNat_add]
no goals
m n k : Nat
⊢ subNatNat (succ m * succ n) (succ m * k) = subNatNat (succ m * succ n + 0) (succ m * k)
rfl
m n k : Nat
⊢ ↑(succ m * succ (succ (n + k))) = ↑(succ m * succ n + succ m * succ k)
m n k : Nat
⊢ -[m+1] * (-[n+1] + -[k+1]) = -[m+1] * -[n+1] + -[m+1] * -[k+1]
simp
m n k : Nat
⊢ ↑(succ m * succ (succ (n + k))) = ↑(succ m * succ (n + succ k))
m n k : Nat
⊢ ↑(succ m * succ (succ (n + k))) = ↑(succ m * succ n + succ m * succ k)
rw [← Nat.left_distrib, succ_add]
no goals
m n k : Nat
⊢ ↑(succ m * succ (succ (n + k))) = ↑(succ m * succ (n + succ k))
rfl