add_left_cancel

formal source

 283
 284/-- Left cancellation: `a + b = a + c ⇒ b = c`. Proved by transferring
 285to `Nat` via the recovery isomorphism. -/
 286theorem add_left_cancel {a b c : LogicNat} (h : a + b = a + c) : b = c := by
 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`. -/
 295theorem add_right_cancel {a b c : LogicNat} (h : a + c = b + c) : a = b := by
 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`. -/
 302theorem eq_iff_toNat_eq {a b : LogicNat} : a = b ↔ toNat a = toNat b := by
 303  constructor
 304  · exact congrArg toNat
 305  · intro h
 306    have := congrArg fromNat h
 307    rw [fromNat_toNat, fromNat_toNat] at this
 308    exact this
 309
 310/-! ## 5b. Order on LogicNat
 311
 312Order is forced by the orbit's cost ordering: in the orbit
 313`{1, γ, γ², ...}` with `γ > 1`, the cost `J(γⁿ)` is strictly
 314increasing in `n`. Section 6's `embed_strictMono` establishes this
 315analytically. Here we define the abstract Peano order intrinsically
 316to `LogicNat` (via existence of an additive complement) so the order