def cmp_dbl

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natcmp.bend:25

import Base

25def cmp_dbl(+a: Nat, +b: Nat) -> {Nat.cmp(Nat.double(a), Nat.double(b)) == Nat.cmp(a, b) : Cmp}:
26  match a b:
27    case 0n 0n:
28      {==}
29    case 0n 1n+ +bp:
30      {==}
31    case 1n+ +ap 0n:
32      {==}
33    case 1n+ +ap 1n+ +bp:
34      cmp_dbl(ap, bp)