def cmp_min

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/natcmp.bend:137

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C

137# a common scale 2^min cancels
138def cmp_min(+a: Nat, +b: Nat, +p: Nat, +q: Nat) -> {Nat.cmp(C.shift(Nat.sub(a, Nat.min(a, b)), p), C.shift(Nat.sub(b, Nat.min(a, b)), q)) == Nat.cmp(C.shift(a, p), C.shift(b, q)) : Cmp}:
139  +m = Nat.min(a, b)
140  +X0 = C.shift(Nat.sub(a, m), p)
141  +Y0 = C.shift(Nat.sub(b, m), q)
142  +e1 = Equal.cong(Nat, Cmp, z => Nat.cmp(z, C.shift(b, q)), C.shift(a, p), C.shift(m, X0), sh_split(a, m, p, min_le_l(a, b)))
143  +e2 = Equal.cong(Nat, Cmp, z => Nat.cmp(C.shift(m, X0), z), C.shift(b, q), C.shift(m, Y0), sh_split(b, m, q, min_le_r(a, b)))
144  Equal.sym(Cmp, Nat.cmp(C.shift(a, p), C.shift(b, q)), Nat.cmp(X0, Y0), Equal.trans(Cmp, Nat.cmp(C.shift(a, p), C.shift(b, q)), Nat.cmp(C.shift(m, X0), C.shift(b, q)), Nat.cmp(X0, Y0), e1, Equal.trans(Cmp, Nat.cmp(C.shift(m, X0), C.shift(b, q)), Nat.cmp(C.shift(m, X0), C.shift(m, Y0)), Nat.cmp(X0, Y0), e2, cmp_shift(m, X0, Y0))))