proposition: Lemma inside_interval_1_dec_inf : forall o1 o2 : Z, {inside_interval_1 o1 o2} + {~ inside_interval_1 o1 o2}.
proof: Proof. intros. abstract (case (Z_lt_dec 0 o1); intro Ho1; [ case (Z_lt_dec 0 o2); intro Ho2; [ left; left; split | right; intro H; match goal with | id1:(~ ?X1) |- ?X2 => apply id1; case H; intros (H1, H2); [ idtac | apply False_ind; apply Z.lt_irrefl with o1; apply Z.lt_trans with 0%Z ] end ] | case (Z_lt_dec o1 0); intro Ho1'; [ case (Z_lt_dec o2 0); intro Ho2; [ left; right; split | right; intro H; case H; intros (H1, H2); [ apply Ho1 | apply Ho2 ] ] | right; intro H; apply Ho1; case H; intros (H1, H2); [ idtac | apply False_ind; apply Ho1' ] ] ]; try assumption). Defined.
imports: Coq(ZArithRing)