def uq.lt_dbl

bend-osdev-algo@0.1.0.0 · proof_u32.bend:122

import Base

122def uq.lt_dbl(x: Nat, y: Nat) -> {Nat.is_lt(Nat.double(x), Nat.double(y)) == Nat.is_lt(x, y) : Bool}:
123  match x y:
124    case 0n 0n:
125      {==}
126    case 0n 1n+q:
127      {==}
128    case 1n+p 0n:
129      {==}
130    case 1n+p 1n+q:
131      uq.lt_dbl(p, q)