def ns.lt_dbl

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

import Base

137def ns.lt_dbl(x: Nat, y: Nat) -> {Nat.is_lt(Nat.double(x), Nat.double(y)) == Nat.is_lt(x, y) : Bool}:
138  match x y:
139    case 0n 0n:
140      {==}
141    case 0n 1n+ +q:
142      {==}
143    case 1n+ +p 0n:
144      {==}
145    case 1n+ +p 1n+ +q:
146      ns.lt_dbl(p, q)