295theorem add_right_cancel {a b c : LogicNat} (h : a + c = b + c) : a = b := by
proof body
Term-mode proof.
296 rw [add_comm a c, add_comm b c] at h 297 exact add_left_cancel h 298 299/-- Transfer principle: an equation in `LogicNat` holds iff it holds 300under `toNat`. This is the workhorse for proofs that route through 301`omega` on `Nat`. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.