move invert_def to comparisonTheory (in HOL)