def lea_mono

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/limbs.bend:96

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

96# a weaker bound
97def lea_mono(+xs: List<&2, U32>, +b: Nat, +c: Nat, +hb: {Nat.is_le(b, c) == True{} : Bool}, +e: {lea(xs, b) == True{} : Bool}) -> {lea(xs, c) == True{} : Bool}:
98  match xs:
99    case Nil{}:
100      {==}
101    case Con{+x, +xt}:
102      L.and_intro(Nat.is_le(v(x), c), lea(xt, c), N.le_trans(v(x), b, c, lea_head(x, xt, b, e), hb), lea_mono(xt, b, c, hb, lea_tail(x, xt, b, e)))