law div_self

bend-mathlib@0.8.1.0 · nat.bend:1920

import Base

1920# A positive natural divided by itself is one: (1 + b) / (1 + b) = 1.
1921law div_self:
1922  for b: Nat
1923  {Nat.div(1n+b, 1n+b) == 1n : Nat}