α : Type ?u.30847
b : PosNum
⊢ 1 + ↑b = ↑1 + ↑b
α : Type ?u.30847
b : PosNum
⊢ ↑(1 + b) = ↑1 + ↑b
rw [one_add b, succ_to_nat, add_comm]
no goals
α : Type ?u.30847
b : PosNum
⊢ 1 + ↑b = ↑1 + ↑b
rfl
α : Type ?u.30847
a : PosNum
⊢ ↑a + 1 = ↑a + ↑1
α : Type ?u.30847
a : PosNum
⊢ ↑(a + 1) = ↑a + ↑1
rw [add_one a, succ_to_nat]
no goals
α : Type ?u.30847
a : PosNum
⊢ ↑a + 1 = ↑a + ↑1
rfl
no goals
α : Type ?u.30847
a b : PosNum
⊢ ↑a + ↑b + (↑a + ↑b) + 1 = ↑a + ↑a + (↑b + ↑b + 1)
simp [add_left_comm]
no goals
α : Type ?u.30847
a b : PosNum
⊢ ↑a + ↑b + (↑a + ↑b) + 1 = ↑a + ↑a + 1 + (↑b + ↑b)
simp [add_comm, add_left_comm]
α : Type ?u.30847
a b : PosNum
⊢ ↑a + ↑b + 1 + (↑a + ↑b + 1) = ↑a + ↑a + 1 + (↑b + ↑b + 1)
α : Type ?u.30847
a b : PosNum
⊢ ↑(succ (a + b)) + ↑(succ (a + b)) = ↑a + ↑a + 1 + (↑b + ↑b + 1)
rw [succ_to_nat, add_to_nat a b]
no goals
α : Type ?u.30847
a b : PosNum
⊢ ↑a + ↑b + 1 + (↑a + ↑b + 1) = ↑a + ↑a + 1 + (↑b + ↑b + 1)
simp [add_left_comm]