include "basics/logic.ma".

inductive compare: Type[0] ≝
  compare_equal: compare
| compare_less: compare
| compare_greater: compare
| compare_less_equal: compare
| compare_greater_equal: compare.