proposition: Lemma Z_dec' : forall n m:Z, {n < m} + {m < n} + {n = m}.
proof: Proof. intros x y. case (Z.eq_dec x y); intro H; [ right; assumption | left; apply (not_Zeq_inf _ _ H) ]. Defined.
imports: Sumbool BinInt Zorder Zcompare