Theorem: QuadRing.coe_nat_add (ECTate/Algebra/QuadRing/Basic.lean)

State before:
F : Type u_1
a b : F
inst✝ : CommRing F
r s : ℕ
⊢ ↑(r + s) = ↑r + ↑s
Tactic:
ext <;> simp only [coe_nat_b1, coe_nat_b2, add_b1, add_b2, Nat.cast_add, add_zero]
State after:
no goals