pith. machine review for the scientific record. sign in
theorem proved tactic proof

add_left_cancel

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 286theorem add_left_cancel {a b c : LogicNat} (h : a + b = a + c) : b = c := by

proof body

Tactic-mode proof.

 287  have hcast := congrArg toNat h
 288  rw [toNat_add, toNat_add] at hcast
 289  have hnat : toNat b = toNat c := by omega
 290  have := congrArg fromNat hnat
 291  rw [fromNat_toNat, fromNat_toNat] at this
 292  exact this
 293
 294/-- Right cancellation: `a + c = b + c ⇒ a = b`. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.