law succ_pred

lawful-fields@0.1.1.0 · proof_num.bend:79

import Base

79law succ_pred:
80  for +M: Nat
81  for +h: {Nat.is_lt(0n, M) == True{} : Bool}
82  {1n+Nat.sub(M, 1n) == M : Nat}