def le_succ

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

import Base

72def le_succ(+n: Nat) -> {Nat.is_le(n, 1n+n) == True{} : Bool}:
73  match n:
74    case 0n:
75      {==}
76    case 1n+p:
77      le_succ(p)