~/jendhub

def wn.cmp_eq

bend-osdev-word64@0.1.1.0 · proof_value.bend:238

import bend-osdev-word64@0.1.1.0/proof_value.bend as ProofValue
import Base

238def wn.cmp_eq(x: Nat, y: Nat, e: {Nat.cmp(x, y) == EQ{} : Cmp}) -> {x == y : Nat}:
239  match x y:
240    case 0n 0n:
241      {==}
242    case 0n 1n+q:
243      Empty.absurd({0n == 1n+q : Nat}, wn.lt_eq(e))
244    case 1n+p 0n:
245      Empty.absurd({1n+p == 0n : Nat}, wn.gt_eq(e))
246    case 1n+p 1n+q:
247      wn.succ_cong(p, q, wn.cmp_eq(p, q, e))

Uses (7)

Used by (1)