proposition: Lemma inside_square_1_dec_inf : forall o1 o2 : Z, {inside_square_1 o1 o2} + {~ inside_square_1 o1 o2}.
proof: Proof. intros. case (Z_lt_dec 2 o1). intro. case (Z_lt_dec 2 o2). intros. left. left. split; repeat assumption. intro. right. intro. apply n. case H. intros (H1, H2). assumption. intros (H1, H2). apply False_ind. apply Z.lt_irrefl with o1. apply Z.lt_trans with (-2)%Z. assumption. apply Z.lt_trans with 2%Z. constructor. assumption. intro. case (Z_lt_dec o1 (-2)). intro. case (Z_lt_dec o2 (-2)). intros. left. right. split; repeat assumption. intro. right. intro. apply n0. case H. intros (H1, H2). apply False_ind. apply Z.lt_irrefl with o1. apply Z.lt_trans with (-2)%Z. assumption. apply Z.lt_trans with 2%Z. constructor. assumption. intros (H1, H2). assumption. intros. right. intro. apply n0. case H. intros (H1, H2). apply False_ind. apply n. assumption. intros (H1, H2). assumption. Qed.
imports: Coq(ZArithRing) QArithSternBrocot(Qhomographic_sign) QArithSternBrocot(Zaux)