proposition: Lemma not_Zeq_inf : forall x y : Z, x <> y -> {(x < y)%Z} + {(y < x)%Z}.
proof: Proof. intros. case Z_lt_ge_dec with x y. intro. left. assumption. intro H0. generalize (Z.ge_le _ _ H0). intro. case (Z_le_lt_eq_dec _ _ H1). intro. right. assumption. intro. apply False_rec. apply H. symmetry in |- *. assumption. Qed.
imports: Coq(Lia)