def len_le_mono

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

57def len_le_mono(+k: Nat, +d: Nat, +xs: List<&2, U32>, +e: {len_le(k, xs) == True{} : Bool}) -> {len_le(Nat.add(k, d), xs) == True{} : Bool}:
58  match k xs:
59    case 0n Nil{}:
60      len_le_nil(d)
61    case 0n Con{y, yt}:
62      Empty.absurd({len_le(d, Con{y, yt}) == True{} : Bool}, L.false_true(e))
63    case 1n+m Nil{}:
64      {==}
65    case 1n+ +m Con{y, +yt}:
66      len_le_mono(m, d, yt, e)