proposition: Lemma Z_dec : forall x y : Z, {(x < y)%Z} + {(x > y)%Z} + {x = y}.
proof: Proof. intros. 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 in |- *. assumption. Qed.
imports: Coq(Lia)