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