def le_value

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64add.bend:199

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU

199def le_value(+a: WU.U64, +b: WU.U64) -> SW.Le.value(a, b):
200  Equal.trans(Bool, Bool.not(X.lt(b, a)), Bool.not(Nat.is_lt(SW.value(b), SW.value(a))), Nat.is_le(SW.value(a), SW.value(b)), Equal.cong(Bool, Bool, t => Bool.not(t), X.lt(b, a), Nat.is_lt(SW.value(b), SW.value(a)), lt_value(b, a)), nle(SW.value(b), SW.value(a), Nat.is_lt(SW.value(b), SW.value(a)), {==}))