law succ_inj

bend-mathlib@0.8.1.0 · nat.bend:141

import Base

141# The successor function is injective: a + 1 = b + 1 implies a = b.
142law succ_inj:
143  for -a: Nat
144  for -b: Nat
145  for e: {1n+a == 1n+b : Nat}
146  {a == b : Nat}