law mul_one

bend-mathlib@0.8.1.0 · nat.bend:223

import Base

223# One is a right identity for multiplication: x * 1 = x.
224law mul_one:
225  for x: Nat
226  {Nat.mul(x, 1n) == x : Nat}