proposition: Lemma Z_dec : forall n m:Z, {n < m} + {n > m} + {n = m}.
proof: Proof. intros x y. case (Z_lt_ge_dec x y). - intro H. left. left. assumption. - intro H. generalize (Z.ge_le _ _ H). intro H0. case (Z_le_lt_eq_dec y x H0). + intro H1. left. right. apply Z.lt_gt. assumption. + intro. right. symmetry . assumption. Defined.
imports: Sumbool BinInt Zorder Zcompare