no goals
m : Nat
b : Int
k : Nat
⊢ ↑m + b + ↑k = ↑m + (b + ↑k)
rw [Int.add_comm, ← aux1, Int.add_comm k, aux1, Int.add_comm b]
no goals
a : Int
n k : Nat
⊢ a + ↑n + ↑k = a + (↑n + ↑k)
rw [Int.add_comm, Int.add_comm a, ← aux1, Int.add_comm a, Int.add_comm k]
no goals
m n k : Nat
⊢ -[m+1] + ↑n + -[k+1] = -[m+1] + (↑n + -[k+1])
rw [Int.add_comm, ← aux2, Int.add_comm n, ← aux2, Int.add_comm -[m+1]]
no goals
m n k : Nat
⊢ ↑m + -[n+1] + -[k+1] = ↑m + (-[n+1] + -[k+1])
rw [Int.add_comm, Int.add_comm m, Int.add_comm m, ← aux2, Int.add_comm -[k+1]]
no goals
m n k : Nat
⊢ -[m+1] + -[n+1] + -[k+1] = -[m+1] + (-[n+1] + -[k+1])
simp [add_succ, Nat.add_comm, Nat.add_left_comm, neg_ofNat_succ]
no goals
x✝² x✝¹ x✝ : Int
m n k : Nat
⊢ ↑m + ↑n + ↑k = ↑m + (↑n + ↑k)
simp [Nat.add_assoc]
no goals
x✝² x✝¹ x✝ : Int
m n k : Nat
⊢ ↑m + ↑n + -[k+1] = ↑m + (↑n + -[k+1])
simp [subNatNat_add]
x✝² x✝¹ x✝ : Int
m n k : Nat
⊢ subNatNat k (succ (succ (m + n))) = -[m+1] + subNatNat k (succ n)
x✝² x✝¹ x✝ : Int
m n k : Nat
⊢ -[m+1] + -[n+1] + ↑k = -[m+1] + (-[n+1] + ↑k)
simp [add_succ]
x✝² x✝¹ x✝ : Int
m n k : Nat
⊢ subNatNat k (succ (succ (m + n))) = subNatNat k (succ n + succ m)
x✝² x✝¹ x✝ : Int
m n k : Nat
⊢ subNatNat k (succ (succ (m + n))) = -[m+1] + subNatNat k (succ n)
rw [Int.add_comm, subNatNat_add_negSucc]
no goals
x✝² x✝¹ x✝ : Int
m n k : Nat
⊢ subNatNat k (succ (succ (m + n))) = subNatNat k (succ n + succ m)
simp [add_succ, succ_add, Nat.add_comm]