proposition: Lemma Zlt_cotrans : forall x y : Z, (x < y)%Z -> forall z : Z, {(x < z)%Z} + {(z < y)%Z}.
proof: Proof. intros. case (Z_lt_ge_dec x z). intro. left. assumption. intro. right. apply Z.le_lt_trans with (m := x). apply Z.ge_le. assumption. assumption. Qed.
imports: Coq(Lia)