def le_refl

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:58

import Base

58def le_refl(+n: Nat) -> {Nat.is_le(n, n) == True{} : Bool}:
59  match n:
60    case 0n:
61      {==}
62    case 1n+p:
63      le_refl(p)