def cmp_addr

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

50def cmp_addr(+a: Nat, +b: Nat, +s: Nat) -> {Nat.cmp(Nat.add(a, s), Nat.add(b, s)) == Nat.cmp(a, b) : Cmp}:
51  +e1 = Equal.cong(Nat, Cmp, z => Nat.cmp(z, Nat.add(b, s)), Nat.add(a, s), Nat.add(s, a), NA.add_comm(a, s))
52  +e2 = Equal.cong(Nat, Cmp, z => Nat.cmp(Nat.add(s, a), z), Nat.add(b, s), Nat.add(s, b), NA.add_comm(b, s))
53  Equal.trans(Cmp, Nat.cmp(Nat.add(a, s), Nat.add(b, s)), Nat.cmp(Nat.add(s, a), Nat.add(b, s)), Nat.cmp(a, b), e1, Equal.trans(Cmp, Nat.cmp(Nat.add(s, a), Nat.add(b, s)), Nat.cmp(Nat.add(s, a), Nat.add(s, b)), Nat.cmp(a, b), e2, cmp_add(s, a, b)))