law one_mul

bend-mathlib@0.8.1.0 · nat.bend:236

import Base

236# One is a left identity for multiplication: 1 * x = x.
237law one_mul:
238  for x: Nat
239  {Nat.mul(1n, x) == x : Nat}