add_right_cancel
plain-language theorem explainer
Right cancellation for addition on LogicNat states that a + c = b + c implies a = b. Researchers deriving Peano-style arithmetic from the logic functional equation cite this when rearranging equations in the forced orbit. The proof is a one-line wrapper that invokes add_comm twice to reduce the claim to the already-proved left-cancellation theorem.
Claim. If $a + c = b + c$ for $a, b, c$ in the logic-forced naturals, then $a = b$.
background
LogicNat is the inductive type whose constructors identity (zero-cost element) and step generate the multiplicative orbit {1, γ, γ², …} forced by the Law of Logic. Addition is defined recursively on this structure so that it satisfies the same recursive equations as ordinary addition on ℕ. The forward map toNat extracts the iteration count, sending identity to 0 and step n to the successor of toNat n, thereby embedding LogicNat into standard Nat arithmetic.
proof idea
The term proof first rewrites the hypothesis by applying add_comm to both sides, converting a + c = b + c into c + a = c + b. It then hands the rewritten equation directly to add_left_cancel, which discharges the goal by transferring to Nat, applying omega, and pulling the equality back via the fromNat/toNat isomorphism.
why it matters
This lemma supplies the symmetric counterpart to add_left_cancel and is required for routine algebraic manipulation inside the foundational arithmetic layer. It is invoked by rev_add_one_eq in GrayCycleBRGC and allOnes_succ_eq_bit in GrayCycleGeneral to handle successor identities in binary-cycle constructions. The result therefore closes a basic cancellation property needed before the transfer principle between LogicNat and Nat can be used freely.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.