def cmp_gt

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

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

87def cmp_gt(+a: Nat, +b: Nat, +h: {Nat.is_lt(b, a) == True{} : Bool}) -> {Nat.cmp(a, b) == GT{} : Cmp}:
88  Equal.trans(Cmp, Nat.cmp(a, b), SF.flip(Nat.cmp(b, a)), GT{}, Equal.sym(Cmp, SF.flip(Nat.cmp(b, a)), Nat.cmp(a, b), cmp_flip(b, a)), Equal.cong(Cmp, Cmp, t => SF.flip(t), Nat.cmp(b, a), LT{}, cmp_lt(b, a, h)))