def lt_succ

bend-collections-laws-math@1.0.0.0 · proofs/lib/nat.bend:65

import Base

65def lt_succ(+n: Nat) -> {Nat.is_lt(n, 1n+n) == True{} : Bool}:
66  match n:
67    case 0n:
68      {==}
69    case 1n+p:
70      lt_succ(p)