def eq_of_cmp

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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

93def eq_of_cmp(+a: Nat, +b: Nat, +h: {Nat.cmp(a, b) == EQ{} : Cmp}) -> {a == b : Nat}:
94  N.eq_from_is_eq(a, b, Equal.cong(Cmp, Bool, t => Cmp.is_eq(t), Nat.cmp(a, b), EQ{}, h))