law div_one

bend-mathlib@0.8.1.0 · nat.bend:1880

import Base

1880# Dividing by one changes nothing: a / 1 = a.
1881law div_one:
1882  for a: Nat
1883  {Nat.div(a, 1n) == a : Nat}