def ns.lt_dbl1

bend-osdev-word64@0.1.1.0 · proof_shift.bend:148

import Base

148def ns.lt_dbl1(x: Nat, y: Nat) -> {Nat.is_lt(1n+Nat.double(x), Nat.double(y)) == Nat.is_lt(x, y) : Bool}:
149  match x y:
150    case 0n 0n:
151      {==}
152    case 0n 1n+ +q:
153      {==}
154    case 1n+ +p 0n:
155      {==}
156    case 1n+ +p 1n+ +q:
157      ns.lt_dbl1(p, q)