323theorem toInt_add (a b : LogicInt) : toInt (a + b) = toInt a + toInt b := by
proof body
Term-mode proof.
324 induction a using Quotient.inductionOn with 325 | h p => 326 induction b using Quotient.inductionOn with 327 | h q => 328 rcases p with ⟨a, b⟩ 329 rcases q with ⟨c, d⟩ 330 show toInt (mk (a + c) (b + d)) = toInt (mk a b) + toInt (mk c d) 331 rw [toInt_mk, toInt_mk, toInt_mk] 332 rw [toNat_add, toNat_add] 333 push_cast 334 ring 335
used by (9)
From the project-wide theorem graph. These declarations reference this one in their body.