proposition: Lemma inside_square_1_inf : forall o1 o2 : Z, inside_square_1 o1 o2 -> {(2 < o1)%Z /\ (2 < o2)%Z} + {(o1 < -2)%Z /\ (o2 < -2)%Z}.
proof: Proof. intros o1 o2 H. case (Z_lt_dec 2 o1); intros Ho1; [ case (Z_lt_dec 2 o2); intros Ho2; [ left; split; assumption | idtac ] | case (Z_lt_dec o1 (-2)); intros Ho1'; [ case (Z_lt_dec o2 (-2)); intros Ho2; [ right; split; assumption | idtac ] | idtac ] ]; apply False_rec; case H; intros (Ho1_, Ho2_); repeat match goal with | id1:(~ (?X1 < ?X2)%Z) |- ?X3 => apply id1; assumption end || match goal with | id1:(Zpos ?X1 < ?X2)%Z,id2:(?X2 < Zneg ?X1)%Z |- ?X3 => apply (Z.lt_irrefl (Zpos X1)); apply Z.lt_trans with (Zneg X1); constructor || apply Z.lt_trans with X2; assumption end. Qed.
imports: Coq(ZArithRing)