law double_inj

bend-mathlib@0.8.1.0 · nat.bend:3785

import Base

3785# Doubling is injective: double a = double b implies a = b.
3786law double_inj:
3787  for a: Nat
3788  for b: Nat
3789  for e: {Nat.double(a) == Nat.double(b) : Nat}
3790  {a == b : Nat}