def len_le_nil

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/poly.bend:50

import Base

50def len_le_nil(+n: Nat) -> {len_le(n, Nil{}) == True{} : Bool}:
51  match n:
52    case 0n:
53      {==}
54    case 1n+m:
55      {==}