def le_trans

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:143

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

143def le_trans(+a: Nat, +b: Nat, +c: Nat, ab: {Nat.is_le(a, b) == True{} : Bool}, bc: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.is_le(a, c) == True{} : Bool}:
144  match a b c:
145    case 0n _ _:
146      zero_le(c)
147    case 1n+p 0n _:
148      Empty.absurd({Nat.is_le(1n+p, c) == True{} : Bool}, L.false_true(ab))
149    case 1n+p 1n+q 0n:
150      Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, L.false_true(bc))
151    case 1n+p 1n+q 1n+r:
152      le_trans(p, q, r, ab, bc)