~/jendhub

def wn.cmp_gt

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

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

227def wn.cmp_gt(x: Nat, y: Nat, h: {Nat.is_lt(y, x) == True{} : Bool}) -> {Nat.cmp(x, y) == GT{} : Cmp}:
228  match x y:
229    case 0n 0n:
230      Empty.absurd({EQ{} == GT{} : Cmp}, wn.ft(h))
231    case 0n 1n+q:
232      Empty.absurd({LT{} == GT{} : Cmp}, wn.ft(h))
233    case 1n+p 0n:
234      {==}
235    case 1n+p 1n+q:
236      wn.cmp_gt(p, q, h)

Uses (7)

Used by (1)