law div_self_sym

bend-mathlib@0.8.1.0 · nat.bend:4391

import Base

4391# A positive natural divided by itself is one: (1 + b) / (1 + b) = 1, reversed to rewrite toward the simple side.
4392law div_self_sym:
4393  for b: Nat
4394  {1n == Nat.div(1n+b, 1n+b) : Nat}