def lt_of_gt

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

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

99def lt_of_gt(+a: Nat, +b: Nat, +h: {Nat.cmp(a, b) == GT{} : Cmp}) -> {Nat.is_lt(b, a) == True{} : Bool}:
100  lt_of_cmp(b, a, Equal.trans(Cmp, Nat.cmp(b, a), SF.flip(Nat.cmp(a, b)), LT{}, Equal.sym(Cmp, SF.flip(Nat.cmp(a, b)), Nat.cmp(b, a), cmp_flip(a, b)), Equal.cong(Cmp, Cmp, t => SF.flip(t), Nat.cmp(a, b), GT{}, h)))