def cmp_flip

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

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF

76def cmp_flip(+a: Nat, +b: Nat) -> {SF.flip(Nat.cmp(a, b)) == Nat.cmp(b, a) : Cmp}:
77  match a b:
78    case 0n 0n:
79      {==}
80    case 0n 1n+ +bp:
81      {==}
82    case 1n+ +ap 0n:
83      {==}
84    case 1n+ +ap 1n+ +bp:
85      cmp_flip(ap, bp)