proposition: Lemma Zlt_cotrans_pos : forall n m:Z, 0 < n + m -> {0 < n} + {0 < m}.
proof: Proof. intros x y H. case (Zlt_cotrans 0 (x + y) H x). - now left. - right. apply (Z.add_lt_mono_l _ _ x). now rewrite Z.add_0_r. Defined.
imports: Sumbool BinInt Zorder Zcompare