def ncmp_flip

bend-kit-collections@0.1.4.1 · PROOF.bend:3964

import Base
import bend-kit-collections@0.1.4.1/LAWS.bend as Laws

3964def ncmp_flip(a: Nat, b: Nat) -> {Nat.cmp(b, a) == Laws.flip(Nat.cmp(a, b)) : Cmp}:
3965  match a b:
3966    case 0n 0n:
3967      {==}
3968    case 0n 1n+q:
3969      {==}
3970    case 1n+p 0n:
3971      {==}
3972    case 1n+p 1n+q:
3973      ncmp_flip(p, q)