def ncmp_trans

bend-kit-collections@0.1.4.1 · PROOF.bend:3975

import Base

3975def ncmp_trans(
3976  a: Nat, b: Nat, c: Nat, e1: {Nat.cmp(a, b) == LT{} : Cmp}, e2: {Nat.cmp(b, c) == LT{} : Cmp}
3977) -> {Nat.cmp(a, c) == LT{} : Cmp}:
3978  match a b c:
3979    case 0n 0n _:
3980      lt_absurd({Nat.cmp(0n, c) == LT{} : Cmp}, EQ{}, {==}, e1)
3981    case 1n+p 0n _:
3982      lt_absurd({Nat.cmp(1n+p, c) == LT{} : Cmp}, GT{}, {==}, e1)
3983    case _ 1n+q 0n:
3984      lt_absurd({Nat.cmp(a, 0n) == LT{} : Cmp}, GT{}, {==}, e2)
3985    case 0n 1n+q 1n+r:
3986      {==}
3987    case 1n+p 1n+q 1n+r:
3988      ncmp_trans(p, q, r, e1, e2)