def uq.lt_dbl1

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

import Base

133def uq.lt_dbl1(x: Nat, y: Nat) -> {Nat.is_lt(1n+Nat.double(x), Nat.double(y)) == Nat.is_lt(x, y) : Bool}:
134  match x y:
135    case 0n 0n:
136      {==}
137    case 0n 1n+q:
138      {==}
139    case 1n+p 0n:
140      {==}
141    case 1n+p 1n+q:
142      uq.lt_dbl1(p, q)