proposition: Lemma Zlt_cotrans_neg : forall n m:Z, n + m < 0 -> {n < 0} + {m < 0}.
proof: Proof. intros x y H; case (Zlt_cotrans (x + y) 0 H x); intro Hxy; [ right; apply (Z.add_lt_mono_l _ _ x); rewrite Z.add_0_r | left ]; assumption. Defined.
imports: Sumbool BinInt Zorder Zcompare