def cmp_lt_gt
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Logicimport Base
72def cmp_lt_gt(e: {LT{} == GT{} : Cmp}) -> Empty:
73 %e : truth(Cmp.is_lt(_))
74 Unit{}
Uses (5)
Used by (0)
No other definition uses this definition.