def ncmp_eq

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

import Base

3952def ncmp_eq(a: Nat, b: Nat, e: {Nat.cmp(a, b) == EQ{} : Cmp}) -> {a == b : Nat}:
3953  match a b:
3954    case 0n 0n:
3955      {==}
3956    case 0n 1n+q:
3957      ne_absurd({0n == 1n+q : Nat}, LT{}, {==}, e)
3958    case 1n+p 0n:
3959      ne_absurd({1n+p == 0n : Nat}, GT{}, {==}, e)
3960    case 1n+p 1n+q:
3961      %ncmp_eq(p, q, e) : {1n+p == 1n+_ : Nat}
3962      {==}