proposition: Theorem Ztrichotomy_inf n m : {n < m} + {n = m} + {n > m}.
proof: Proof. unfold ">", "<". generalize (Z.compare_eq n m). destruct (n ?= m); [ left; right | left; left | right]; auto. Defined.
imports: BinPos BinInt Decidable Zcompare Arith_base