law lt_one

lawful-words@0.1.0.0 · proof_word.bend:1051

import Base

1051# x < 1 gives x = 0.
1052law lt_one:
1053  for +x: Nat
1054  for +h: {Nat.is_lt(x, 1n) == True{} : Bool}
1055  {x == 0n : Nat}