law lt_one

lawful-arrays@0.1.0.0 · proof_base.bend:156

import Base

156# Below 1 is 0.
157law lt_one:
158  for +k: Nat
159  for e: {Nat.is_lt(k, 1n) == True{} : Bool}
160  {k == 0n : Nat}