law div_one

lawful-words@0.1.0.0 · proof_nat.bend:1145

import Base

1145law div_one:
1146  for +a: Nat
1147  {Nat.div(a, 1n) == a : Nat}