proposition: Lemma Zlt_cotrans_neg : forall x y : Z, (x + y < 0)%Z -> {(x < 0)%Z} + {(y < 0)%Z}.
proof: Proof. intros x y H; case (Zlt_cotrans (x + y) 0 H x); intro Hxy; [ right; apply Zplus_lt_reg_l with (p := x); rewrite Zplus_0_r | left ]; assumption. Qed.
imports: Coq(Lia)