def eq_order

bend-collections-laws-math@1.0.0.0 · proofs/math/u64/u64.bend:126

import Base
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as U

126def eq_order(+c: Cmp, +d: Cmp) -> {Cmp.is_eq(U.order(c, d)) == Bool.and(Cmp.is_eq(d), Cmp.is_eq(c)) : Bool}:
127  match c d:
128    case LT{} LT{}:
129      {==}
130    case LT{} EQ{}:
131      {==}
132    case LT{} GT{}:
133      {==}
134    case EQ{} LT{}:
135      {==}
136    case EQ{} EQ{}:
137      {==}
138    case EQ{} GT{}:
139      {==}
140    case GT{} LT{}:
141      {==}
142    case GT{} EQ{}:
143      {==}
144    case GT{} GT{}:
145      {==}