proposition: Lemma Zlt_cotrans : forall n m:Z, n < m -> forall p:Z, {n < p} + {p < m}.
proof: Proof. intros x y H z. case (Z_lt_ge_dec x z). - intro. left. assumption. - intro. right. apply (Z.le_lt_trans _ x). + apply Z.ge_le. assumption. + assumption. Defined.
imports: Sumbool BinInt Zorder Zcompare