add_right_cancel
plain-language theorem explainer
Right cancellation holds for addition on DistinctionNat: a+c=b+c implies a=b. Cited by anyone transferring Nat-style cancellation into orbit arithmetic, Gray-cycle bit lemmas, or tick-fiber mass identities. The proof is a short commute-then-left-cancel reduction.
Claim. For distinction-orbit positions $a,b,c$, if $a+c=b+c$ then $a=b$.
background
DistinctionNat (K2.12) is the inductive carrier for the base-neutral finite orbit of repeated distinction: constructors zero and succ. OrbitArithmetic equips it with addition by nested succession, with the usual zero/succ rewrite lemmas and commutativity already in place as siblings.
The local setting is primitive recognition calculus arithmetic on that orbit, parallel to LogicNat in ArithmeticFromLogic. Upstream left cancellation states that $c+a=c+b$ implies $a=b$; the LogicNat twin of right cancellation is proved the same way (commute, then left-cancel), and the orbit version mirrors that pattern rather than routing through a toNat recovery map.
proof idea
Apply left cancellation with the common summand placed on the left as $c$. Rewrite both sides of the goal hypothesis by commutativity so $c+a$ and $c+b$ appear; the given equality $a+c=b+c$ then matches the left-cancellation premise exactly. No induction and no transfer to ordinary Nat.
why it matters
Closes K4.5 (right cancellation for orbit addition) in the PRC arithmetic ladder, so later orbit algebra can cancel freely. Downstream it is reused by ArithmeticFromLogic's own right-cancellation statement, by SevenGaps bridges that equate tick-fiber masses under tail fiber shift ($p\mapsto p+1$) and antipodal shift ($p\mapsto p+4$), and by Gray-cycle lemmas that rearrange Fin/Nat successor identities. Those gravity bridges sit on the eight-tick octave (T7) side of the forcing chain; clean cancellation on DistinctionNat keeps the discrete mass-counting steps honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.