law div_one_sym

bend-mathlib@0.8.1.0 · nat.bend:4367

import Base

4367# Dividing by one changes nothing: a / 1 = a, reversed to rewrite toward the simple side.
4368law div_one_sym:
4369  for a: Nat
4370  {a == Nat.div(a, 1n) : Nat}