add_right_cancel

formal source

 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
 317content does not depend on which generator was used. The connection
 318back to the orbit is `embed_le_iff` in Section 6.
 319
 320The standard Peano definition: `n ≤ m` iff there exists `k` with
 321`n + k = m`. Strict order: `n < m` iff there exists `k` with
 322`n + step k = m`. -/
 323
 324/-- Non-strict order on `LogicNat`. -/
 325def le (n m : LogicNat) : Prop := ∃ k : LogicNat, n + k = m