def okb_mono

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

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
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM

90def okb_mono(+n: Nat, +xs: List<&2, U32>, +b: Nat, +c: Nat, +hb: {Nat.is_le(b, c) == True{} : Bool}, +e: {LM.okb(n, xs, b) == True{} : Bool}) -> {LM.okb(n, xs, c) == True{} : Bool}:
91  match n xs:
92    case 0n Nil{}:
93      {==}
94    case 0n Con{y, yt}:
95      Empty.absurd({LM.okb(0n, Con{y, yt}, c) == True{} : Bool}, L.false_true(e))
96    case 1n+m Nil{}:
97      Empty.absurd({LM.okb(1n+m, Nil{}, c) == True{} : Bool}, L.false_true(e))
98    case 1n+ +m Con{+y, +yt}:
99      L.and_intro(Nat.is_le(v(y), c), LM.okb(m, yt, c), N.le_trans(v(y), b, c, LM.okb_head(m, y, yt, b, e), hb), okb_mono(m, yt, b, c, hb, LM.okb_tail(m, y, yt, b, e)))