proposition: Lemma Qquadratic_sign_neg_1 : forall (a b c d e f g h : Z) (p1 p2 : Qpositive) (H_Qquadratic_sg_denom_nonzero : Qquadratic_sg_denom_nonzero e f g h p1 p2) (na nb nc nd ne nf ng nh : Z) (np1 np2 : Qpositive), Qquadratic_sign a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero = ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) -> {(0 < na + nb + nc + nd)%Z /\ (ne + nf + ng + nh < 0)%Z} + {(na + nb + nc + nd < 0 < ne + nf + ng + nh)%Z}.
proof: Proof. fix Qquadratic_sign_neg_1 9. intros. set (o1 := outside_square a b c d) in *. set (o2 := outside_square e f g h) in *. destruct p1 as [xs| xs| ]. destruct p2 as [ys| ys| ]. case (three_integers_dec_inf b c d). intros (Hb, (Hc, Hd)). case (three_integers_dec_inf f g h). intros (Hf, (Hg, Hh)). generalize (Qquadratic_sign_nRdL_nRdL_1 a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = ((Z.sgn a * Z.sgn e)%Z, (a, (b, (c, d)), (e, (f, (g, h))), (nR xs, nR ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. rewrite <- Zsgn_15 in hl. case (Zsgn_17 _ _ (sym_eq hl)); intros (Ha, He); [ left | right ]; repeat split; repeat match goal with | id1:(?X1 = 0%Z) |- ?X2 => rewrite id1; clear id1 end; repeat rewrite Zplus_0_r; assumption. intros H_fgh'. case (Z_lt_dec 2 o2). intro Ho2. generalize (Qquadratic_sign_nRdL_nRdL_2 a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = (Z.sgn a, (a, (b, (c, d)), (e, (f, (g, h))), (nR xs, nR ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. right; split; repeat match goal with | id1:(?X1 = 0%Z) |- ?X2 => rewrite id1; clear id1 end; repeat rewrite Zplus_0_r; [ apply Zsgn_10; apply sym_eq | apply outside_square_1 ]; assumption. case (Z_lt_dec o2 (-2)). intros Ho2' Ho2. generalize (Qquadratic_sign_nRdL_nRdL_3 a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = ((- Z.sgn a)%Z, (a, (b, (c, d)), (e, (f, (g, h))), (nR xs, nR ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. left; split; repeat match goal with | id1:(?X1 = 0%Z) |- ?X2 => rewrite id1; clear id1 end; repeat rewrite Zplus_0_r; [ apply Zsgn_9; apply sym_eq; apply Z.opp_inj; assumption | apply outside_square_2; assumption ]. intros Ho2' Ho2. generalize (Qquadratic_sign_nR_nR_4 a b c d e f g h (nR xs) xs (nR ys) ys H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_1 _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _)). intros H1. assert (H_tuple_eq : Qquadratic_sign a (a + b) (a + c) (a + b + c + d) e (e + f) (e + g) (e + f + g + h) xs ys (Qquadratic_signok_1 e f g h xs ys H_Qquadratic_sg_denom_nonzero) = ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq; apply H1; repeat split | idtac ] | apply (Qquadratic_sign_neg_1 a (a + b)%Z (a + c)%Z (a + b + c + d)%Z e (e + f)%Z (e + g)%Z (e + f + g + h)%Z xs ys (Qquadratic_signok_1 e f g h xs ys H_Qquadratic_sg_denom_nonzero) na nb nc nd ne nf ng nh np1 np2) ]; assumption. intros Hbcd'. case (three_integers_dec_inf f g h). intros (Hf, (Hg, Hh)). case (Z_lt_dec 2 o1). intro Ho1. generalize (Qquadratic_sign_nRdL_nRdL_5 a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = (Z.sgn e, (a, (b, (c, d)), (e, (f, (g, h))), (nR xs, nR ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. left; split; repeat match goal with | id1:(?X1 = 0%Z) |- ?X2 => rewrite id1; clear id1 end; repeat rewrite Zplus_0_r; [ apply outside_square_1 | apply Zsgn_10; apply sym_eq ]; assumption. case (Z_lt_dec o1 (-2)). intros Ho1' Ho1. generalize (Qquadratic_sign_nRdL_nRdL_6 a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = ((- Z.sgn e)%Z, (a, (b, (c, d)), (e, (f, (g, h))), (nR xs, nR ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. right; split; repeat match goal with | id1:(?X1 = 0%Z) |- ?X2 => rewrite id1; clear id1 end; repeat rewrite Zplus_0_r; [ apply outside_square_2 | apply Zsgn_9; apply sym_eq; apply Z.opp_inj ]; assumption. intros Ho2' Ho2. generalize (Qquadratic_sign_nR_nR_7 a b c d e f g h (nR xs) xs (nR ys) ys H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_1 _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _)). intros H1. assert (H_tuple_eq : Qquadratic_sign a (a + b) (a + c) (a + b + c + d) e (e + f) (e + g) (e + f + g + h) xs ys (Qquadratic_signok_1 e f g h xs ys H_Qquadratic_sg_denom_nonzero) = ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq; apply H1; repeat split | idtac ] | apply (Qquadratic_sign_neg_1 a (a + b)%Z (a + c)%Z (a + b + c + d)%Z e (e + f)%Z (e + g)%Z (e + f + g + h)%Z xs ys (Qquadratic_signok_1 e f g h xs ys H_Qquadratic_sg_denom_nonzero) na nb nc nd ne nf ng nh np1 np2) ]; assumption. intro Hfgh'. case (inside_square_1_dec_inf o1 o2). intro H_inside_1. generalize (Qquadratic_sign_nRdL_nRdL_8 a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = (1%Z, (a, (b, (c, d)), (e, (f, (g, h))), (nR xs, nR ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. discriminate hl. intro H_inside_1'. case (inside_square_2_dec_inf o1 o2). intro H_inside_2. generalize (Qquadratic_sign_nRdL_nRdL_9 a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = ((-1)%Z, (a, (b, (c, d)), (e, (f, (g, h))), (nR xs, nR ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. case (inside_square_2_inf _ _ H_inside_2); intros (Ho1, Ho2); [ left; split; [ apply outside_square_1 | apply outside_square_2 ] | right; split; [ apply outside_square_2 | apply outside_square_1 ] ]; assumption. intros H_inside_2'. generalize (Qquadratic_sign_nR_nR_10 a b c d e f g h (nR xs) xs (nR ys) ys H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_1 _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _)). intros H1. assert (H_tuple_eq : Qquadratic_sign a (a + b) (a + c) (a + b + c + d) e (e + f) (e + g) (e + f + g + h) xs ys (Qquadratic_signok_1 e f g h xs ys H_Qquadratic_sg_denom_nonzero) = ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq; apply H1; repeat split | idtac ] | apply (Qquadratic_sign_neg_1 a (a + b)%Z (a + c)%Z (a + b + c + d)%Z e (e + f)%Z (e + g)%Z (e + f + g + h)%Z xs ys (Qquadratic_signok_1 e f g h xs ys H_Qquadratic_sg_denom_nonzero) na nb nc nd ne nf ng nh np1 np2) ]; assumption. case (three_integers_dec_inf b c d). intros (Hb, (Hc, Hd)). case (three_integers_dec_inf f g h). intros (Hf, (Hg, Hh)). generalize (Qquadratic_sign_nRdL_nRdL_1 a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = ((Z.sgn a * Z.sgn e)%Z, (a, (b, (c, d)), (e, (f, (g, h))), (nR xs, dL ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. rewrite <- Zsgn_15 in hl. case (Zsgn_17 _ _ (sym_eq hl)); intros (Ha, He); [ left | right ]; repeat split; repeat match goal with | id1:(?X1 = 0%Z) |- ?X2 => rewrite id1; clear id1 end; repeat rewrite Zplus_0_r; assumption. intros H_fgh'. case (Z_lt_dec 2 o2). intro Ho2. generalize (Qquadratic_sign_nRdL_nRdL_2 a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = (Z.sgn a, (a, (b, (c, d)), (e, (f, (g, h))), (nR xs, dL ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. right; split; repeat match goal with | id1:(?X1 = 0%Z) |- ?X2 => rewrite id1; clear id1 end; repeat rewrite Zplus_0_r; [ apply Zsgn_10; apply sym_eq; assumption | apply outside_square_1; assumption ]. case (Z_lt_dec o2 (-2)). intros Ho2' Ho2. generalize (Qquadratic_sign_nRdL_nRdL_3 a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = ((- Z.sgn a)%Z, (a, (b, (c, d)), (e, (f, (g, h))), (nR xs, dL ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. left; split; repeat match goal with | id1:(?X1 = 0%Z) |- ?X2 => rewrite id1; clear id1 end; repeat rewrite Zplus_0_r; [ apply Zsgn_9; apply sym_eq; apply Z.opp_inj; assumption | apply outside_square_2; assumption ]. intros Ho2' Ho2. generalize (Qquadratic_sign_nR_dL_4 a b c d e f g h (nR xs) xs (dL ys) ys H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_2 _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _)). intros H1. assert (H_tuple_eq : Qquadratic_sign (a + b) b (a + b + c + d) (b + d) (e + f) f (e + f + g + h) (f + h) xs ys (Qquadratic_signok_2 e f g h xs ys H_Qquadratic_sg_denom_nonzero) = ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq; apply H1; repeat split | idtac ] | apply (Qquadratic_sign_neg_1 (a + b)%Z b (a + b + c + d)%Z (b + d)%Z (e + f)%Z f (e + f + g + h)%Z (f + h)%Z xs ys (Qquadratic_signok_2 e f g h xs ys H_Qquadratic_sg_denom_nonzero) na nb nc nd ne nf ng nh np1 np2) ]; assumption. intros Hbcd'. case (three_integers_dec_inf f g h). intros (Hf, (Hg, Hh)). case (Z_lt_dec 2 o1). intro Ho1. generalize (Qquadratic_sign_nRdL_nRdL_5 a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = (Z.sgn e, (a, (b, (c, d)), (e, (f, (g, h))), (nR xs, dL ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. left; split; repeat match goal with | id1:(?X1 = 0%Z) |- ?X2 => rewrite id1; clear id1 end; repeat rewrite Zplus_0_r; [ apply outside_square_1 | apply Zsgn_10; apply sym_eq ]; assumption. case (Z_lt_dec o1 (-2)). intros Ho1' Ho1. generalize (Qquadratic_sign_nRdL_nRdL_6 a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = ((- Z.sgn e)%Z, (a, (b, (c, d)), (e, (f, (g, h))), (nR xs, dL ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. right; split; repeat match goal with | id1:(?X1 = 0%Z) |- ?X2 => rewrite id1; clear id1 end; repeat rewrite Zplus_0_r; [ apply outside_square_2 | apply Zsgn_9; apply sym_eq; apply Z.opp_inj ]; assumption. intros Ho2' Ho2. generalize (Qquadratic_sign_nR_dL_7 a b c d e f g h (nR xs) xs (dL ys) ys H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_2 _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _)). intros H1. assert (H_tuple_eq : Qquadratic_sign (a + b) b (a + b + c + d) (b + d) (e + f) f (e + f + g + h) (f + h) xs ys (Qquadratic_signok_2 e f g h xs ys H_Qquadratic_sg_denom_nonzero) = ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq; apply H1; repeat split | idtac ] | apply (Qquadratic_sign_neg_1 (a + b)%Z b (a + b + c + d)%Z (b + d)%Z (e + f)%Z f (e + f + g + h)%Z (f + h)%Z xs ys (Qquadratic_signok_2 e f g h xs ys H_Qquadratic_sg_denom_nonzero) na nb nc nd ne nf ng nh np1 np2) ]; assumption. intro Hfgh'. case (inside_square_1_dec_inf o1 o2). intro H_inside_1. generalize (Qquadratic_sign_nRdL_nRdL_8 a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = (1%Z, (a, (b, (c, d)), (e, (f, (g, h))), (nR xs, dL ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. discriminate hl. intro H_inside_1'. case (inside_square_2_dec_inf o1 o2). intro H_inside_2. generalize (Qquadratic_sign_nRdL_nRdL_9 a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = ((-1)%Z, (a, (b, (c, d)), (e, (f, (g, h))), (nR xs, dL ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. case (inside_square_2_inf _ _ H_inside_2); intros (Ho1, Ho2); [ left; split; [ apply outside_square_1 | apply outside_square_2 ] | right; split; [ apply outside_square_2 | apply outside_square_1 ] ]; assumption. intros H_inside_2'. generalize (Qquadratic_sign_nR_dL_10 a b c d e f g h (nR xs) xs (dL ys) ys H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_2 _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _)). intros H1. assert (H_tuple_eq : Qquadratic_sign (a + b) b (a + b + c + d) (b + d) (e + f) f (e + f + g + h) (f + h) xs ys (Qquadratic_signok_2 e f g h xs ys H_Qquadratic_sg_denom_nonzero) = ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq; apply H1; repeat split | idtac ] | apply (Qquadratic_sign_neg_1 (a + b)%Z b (a + b + c + d)%Z (b + d)%Z (e + f)%Z f (e + f + g + h)%Z (f + h)%Z xs ys (Qquadratic_signok_2 e f g h xs ys H_Qquadratic_sg_denom_nonzero) na nb nc nd ne nf ng nh np1 np2) ]; assumption. generalize (Qquadratic_signok_0' _ _ _ _ _ H_Qquadratic_sg_denom_nonzero). intros H_Qhomographic_sg_denom_nonzero. set (L3 := Qhomographic_sign (a + b) (c + d) (e + f) (g + h) (nR xs) H_Qhomographic_sg_denom_nonzero) in *. set (l1 := fst L3) in *. set (l2 := fst (snd L3)) in *. set (l3 := snd (snd L3)) in *. set (na_ := fst l2) in *. set (nb_ := fst (snd l2)) in *. set (nc_ := fst (snd (snd l2))) in *. set (nd_ := snd (snd (snd l2))) in *. generalize (Qquadratic_sign_nRdL_One a b c d e f g h (nR xs) One H_Qquadratic_sg_denom_nonzero l1 na_ nb_ nc_ nd_ l3 H_Qhomographic_sg_denom_nonzero); intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = (l1, (0%Z, (na_, (0%Z, nb_)), (0%Z, (nc_, (0%Z, nd_))), (l3, One)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (nR xs) One H_Qquadratic_sg_denom_nonzero); [ apply sym_eq; assumption | apply H1; fold L3 in |- *; repeat (apply pair_2; try reflexivity); discriminate || reflexivity ] | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end; repeat rewrite ZERO_left; repeat rewrite Zplus_0_r ]; apply (sg_neg_1 (a + b) (c + d) (e + f) (g + h) (nR xs) H_Qhomographic_sg_denom_nonzero na_ nb_ nc_ nd_ l3); rewrite hl; fold L3 in |- *; repeat (apply pair_2; try reflexivity); discriminate || reflexivity. destruct p2 as [ys| ys| ]. case (three_integers_dec_inf b c d). intros (Hb, (Hc, Hd)). case (three_integers_dec_inf f g h). intros (Hf, (Hg, Hh)). generalize (Qquadratic_sign_nRdL_nRdL_1 a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = ((Z.sgn a * Z.sgn e)%Z, (a, (b, (c, d)), (e, (f, (g, h))), (dL xs, nR ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. rewrite <- Zsgn_15 in hl. case (Zsgn_17 _ _ (sym_eq hl)); intros (Ha, He); [ left | right ]; repeat split; repeat match goal with | id1:(?X1 = 0%Z) |- ?X2 => rewrite id1; clear id1 end; repeat rewrite Zplus_0_r; assumption. intros H_fgh'. case (Z_lt_dec 2 o2). intro Ho2. generalize (Qquadratic_sign_nRdL_nRdL_2 a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = (Z.sgn a, (a, (b, (c, d)), (e, (f, (g, h))), (dL xs, nR ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. right; split; repeat match goal with | id1:(?X1 = 0%Z) |- ?X2 => rewrite id1; clear id1 end; repeat rewrite Zplus_0_r; [ apply Zsgn_10; apply sym_eq | apply outside_square_1 ]; assumption. case (Z_lt_dec o2 (-2)). intros Ho2' Ho2. generalize (Qquadratic_sign_nRdL_nRdL_3 a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = ((- Z.sgn a)%Z, (a, (b, (c, d)), (e, (f, (g, h))), (dL xs, nR ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. left; split; repeat match goal with | id1:(?X1 = 0%Z) |- ?X2 => rewrite id1; clear id1 end; repeat rewrite Zplus_0_r; [ apply Zsgn_9; apply sym_eq; apply Z.opp_inj; assumption | apply outside_square_2; assumption ]. intros Ho2' Ho2. generalize (Qquadratic_sign_dL_nR_4 a b c d e f g h (dL xs) xs (nR ys) ys H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_3 _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _)). intros H1. assert (H_tuple_eq : Qquadratic_sign (a + c) (a + b + c + d) c (c + d) (e + g) (e + f + g + h) g (g + h) xs ys (Qquadratic_signok_3 e f g h xs ys H_Qquadratic_sg_denom_nonzero) = ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq; apply H1; repeat split | idtac ] | apply (Qquadratic_sign_neg_1 (a + c)%Z (a + b + c + d)%Z c (c + d)%Z (e + g)%Z (e + f + g + h)%Z g (g + h)%Z xs ys (Qquadratic_signok_3 e f g h xs ys H_Qquadratic_sg_denom_nonzero) na nb nc nd ne nf ng nh np1 np2) ]; assumption. intros Hbcd'. case (three_integers_dec_inf f g h). intros (Hf, (Hg, Hh)). case (Z_lt_dec 2 o1). intro Ho1. generalize (Qquadratic_sign_nRdL_nRdL_5 a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = (Z.sgn e, (a, (b, (c, d)), (e, (f, (g, h))), (dL xs, nR ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. left; split; repeat match goal with | id1:(?X1 = 0%Z) |- ?X2 => rewrite id1; clear id1 end; repeat rewrite Zplus_0_r; [ apply outside_square_1 | apply Zsgn_10; apply sym_eq ]; assumption. case (Z_lt_dec o1 (-2)). intros Ho1' Ho1. generalize (Qquadratic_sign_nRdL_nRdL_6 a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = ((- Z.sgn e)%Z, (a, (b, (c, d)), (e, (f, (g, h))), (dL xs, nR ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. right; split; repeat match goal with | id1:(?X1 = 0%Z) |- ?X2 => rewrite id1; clear id1 end; repeat rewrite Zplus_0_r; [ apply outside_square_2 | apply Zsgn_9; apply sym_eq; apply Z.opp_inj ]; assumption. intros Ho2' Ho2. generalize (Qquadratic_sign_dL_nR_7 a b c d e f g h (dL xs) xs (nR ys) ys H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_3 _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _)). intros H1. assert (H_tuple_eq : Qquadratic_sign (a + c) (a + b + c + d) c (c + d) (e + g) (e + f + g + h) g (g + h) xs ys (Qquadratic_signok_3 e f g h xs ys H_Qquadratic_sg_denom_nonzero) = ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq; apply H1; repeat split | idtac ] | apply (Qquadratic_sign_neg_1 (a + c)%Z (a + b + c + d)%Z c (c + d)%Z (e + g)%Z (e + f + g + h)%Z g (g + h)%Z xs ys (Qquadratic_signok_3 e f g h xs ys H_Qquadratic_sg_denom_nonzero) na nb nc nd ne nf ng nh np1 np2) ]; assumption. intro Hfgh'. case (inside_square_1_dec_inf o1 o2). intro H_inside_1. generalize (Qquadratic_sign_nRdL_nRdL_8 a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = (1%Z, (a, (b, (c, d)), (e, (f, (g, h))), (dL xs, nR ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. discriminate hl. intro H_inside_1'. case (inside_square_2_dec_inf o1 o2). intro H_inside_2. generalize (Qquadratic_sign_nRdL_nRdL_9 a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = ((-1)%Z, (a, (b, (c, d)), (e, (f, (g, h))), (dL xs, nR ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. case (inside_square_2_inf _ _ H_inside_2); intros (Ho1, Ho2); [ left; split; [ apply outside_square_1 | apply outside_square_2 ] | right; split; [ apply outside_square_2 | apply outside_square_1 ] ]; assumption. intros H_inside_2'. generalize (Qquadratic_sign_dL_nR_10 a b c d e f g h (dL xs) xs (nR ys) ys H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_3 _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _)). intros H1. assert (H_tuple_eq : Qquadratic_sign (a + c) (a + b + c + d) c (c + d) (e + g) (e + f + g + h) g (g + h) xs ys (Qquadratic_signok_3 e f g h xs ys H_Qquadratic_sg_denom_nonzero) = ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq; apply H1; repeat split | idtac ] | apply (Qquadratic_sign_neg_1 (a + c)%Z (a + b + c + d)%Z c (c + d)%Z (e + g)%Z (e + f + g + h)%Z g (g + h)%Z xs ys (Qquadratic_signok_3 e f g h xs ys H_Qquadratic_sg_denom_nonzero) na nb nc nd ne nf ng nh np1 np2) ]; assumption. case (three_integers_dec_inf b c d). intros (Hb, (Hc, Hd)). case (three_integers_dec_inf f g h). intros (Hf, (Hg, Hh)). generalize (Qquadratic_sign_nRdL_nRdL_1 a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = ((Z.sgn a * Z.sgn e)%Z, (a, (b, (c, d)), (e, (f, (g, h))), (dL xs, dL ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. rewrite <- Zsgn_15 in hl. case (Zsgn_17 _ _ (sym_eq hl)); intros (Ha, He); [ left | right ]; repeat split; repeat match goal with | id1:(?X1 = 0%Z) |- ?X2 => rewrite id1; clear id1 end; repeat rewrite Zplus_0_r; assumption. intros H_fgh'. case (Z_lt_dec 2 o2). intro Ho2. generalize (Qquadratic_sign_nRdL_nRdL_2 a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = (Z.sgn a, (a, (b, (c, d)), (e, (f, (g, h))), (dL xs, dL ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. right; split; repeat match goal with | id1:(?X1 = 0%Z) |- ?X2 => rewrite id1; clear id1 end; repeat rewrite Zplus_0_r; [ apply Zsgn_10; apply sym_eq; assumption | apply outside_square_1; assumption ]. case (Z_lt_dec o2 (-2)). intros Ho2' Ho2. generalize (Qquadratic_sign_nRdL_nRdL_3 a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = ((- Z.sgn a)%Z, (a, (b, (c, d)), (e, (f, (g, h))), (dL xs, dL ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. left; split; repeat match goal with | id1:(?X1 = 0%Z) |- ?X2 => rewrite id1; clear id1 end; repeat rewrite Zplus_0_r; [ apply Zsgn_9; apply sym_eq; apply Z.opp_inj; assumption | apply outside_square_2; assumption ]. intros Ho2' Ho2. generalize (Qquadratic_sign_dL_dL_4 a b c d e f g h (dL xs) xs (dL ys) ys H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_4 _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _)). intros H1. assert (H_tuple_eq : Qquadratic_sign (a + b + c + d) (b + d) (c + d) d (e + f + g + h) (f + h) (g + h) h xs ys (Qquadratic_signok_4 e f g h xs ys H_Qquadratic_sg_denom_nonzero) = ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq; apply H1; repeat split | idtac ] | apply (Qquadratic_sign_neg_1 (a + b + c + d)%Z (b + d)%Z (c + d)%Z d (e + f + g + h)%Z (f + h)%Z (g + h)%Z h xs ys (Qquadratic_signok_4 e f g h xs ys H_Qquadratic_sg_denom_nonzero) na nb nc nd ne nf ng nh np1 np2) ]; assumption. intros Hbcd'. case (three_integers_dec_inf f g h). intros (Hf, (Hg, Hh)). case (Z_lt_dec 2 o1). intro Ho1. generalize (Qquadratic_sign_nRdL_nRdL_5 a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = (Z.sgn e, (a, (b, (c, d)), (e, (f, (g, h))), (dL xs, dL ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. left; split; repeat match goal with | id1:(?X1 = 0%Z) |- ?X2 => rewrite id1; clear id1 end; repeat rewrite Zplus_0_r; [ apply outside_square_1 | apply Zsgn_10; apply sym_eq ]; assumption. case (Z_lt_dec o1 (-2)). intros Ho1' Ho1. generalize (Qquadratic_sign_nRdL_nRdL_6 a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = ((- Z.sgn e)%Z, (a, (b, (c, d)), (e, (f, (g, h))), (dL xs, dL ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. right; split; repeat match goal with | id1:(?X1 = 0%Z) |- ?X2 => rewrite id1; clear id1 end; repeat rewrite Zplus_0_r; [ apply outside_square_2 | apply Zsgn_9; apply sym_eq; apply Z.opp_inj ]; assumption. intros Ho2' Ho2. generalize (Qquadratic_sign_dL_dL_7 a b c d e f g h (dL xs) xs (dL ys) ys H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_4 _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _)). intros H1. assert (H_tuple_eq : Qquadratic_sign (a + b + c + d) (b + d) (c + d) d (e + f + g + h) (f + h) (g + h) h xs ys (Qquadratic_signok_4 e f g h xs ys H_Qquadratic_sg_denom_nonzero) = ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq; apply H1; repeat split | idtac ] | apply (Qquadratic_sign_neg_1 (a + b + c + d)%Z (b + d)%Z (c + d)%Z d (e + f + g + h)%Z (f + h)%Z (g + h)%Z h xs ys (Qquadratic_signok_4 e f g h xs ys H_Qquadratic_sg_denom_nonzero) na nb nc nd ne nf ng nh np1 np2) ]; assumption. intro Hfgh'. case (inside_square_1_dec_inf o1 o2). intro H_inside_1. generalize (Qquadratic_sign_nRdL_nRdL_8 a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = (1%Z, (a, (b, (c, d)), (e, (f, (g, h))), (dL xs, dL ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. discriminate hl. intro H_inside_1'. case (inside_square_2_dec_inf o1 o2). intro H_inside_2. generalize (Qquadratic_sign_nRdL_nRdL_9 a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero). intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = ((-1)%Z, (a, (b, (c, d)), (e, (f, (g, h))), (dL xs, dL ys)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq | apply H1; discriminate || (repeat split) ]; assumption | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end ]. case (inside_square_2_inf _ _ H_inside_2); intros (Ho1, Ho2); [ left; split; [ apply outside_square_1 | apply outside_square_2 ] | right; split; [ apply outside_square_2 | apply outside_square_1 ] ]; assumption. intros H_inside_2'. generalize (Qquadratic_sign_dL_dL_10 a b c d e f g h (dL xs) xs (dL ys) ys H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_4 _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _)). intros H1. assert (H_tuple_eq : Qquadratic_sign (a + b + c + d) (b + d) (c + d) d (e + f + g + h) (f + h) (g + h) h xs ys (Qquadratic_signok_4 e f g h xs ys H_Qquadratic_sg_denom_nonzero) = ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero); [ apply sym_eq; apply H1; repeat split | idtac ] | apply (Qquadratic_sign_neg_1 (a + b + c + d)%Z (b + d)%Z (c + d)%Z d (e + f + g + h)%Z (f + h)%Z (g + h)%Z h xs ys (Qquadratic_signok_4 e f g h xs ys H_Qquadratic_sg_denom_nonzero) na nb nc nd ne nf ng nh np1 np2) ]; assumption. generalize (Qquadratic_signok_0' _ _ _ _ _ H_Qquadratic_sg_denom_nonzero). intros H_Qhomographic_sg_denom_nonzero. set (L3 := Qhomographic_sign (a + b) (c + d) (e + f) (g + h) (dL xs) H_Qhomographic_sg_denom_nonzero) in *. set (l1 := fst L3) in *. set (l2 := fst (snd L3)) in *. set (l3 := snd (snd L3)) in *. set (na_ := fst l2) in *. set (nb_ := fst (snd l2)) in *. set (nc_ := fst (snd (snd l2))) in *. set (nd_ := snd (snd (snd l2))) in *. generalize (Qquadratic_sign_nRdL_One a b c d e f g h (dL xs) One H_Qquadratic_sg_denom_nonzero l1 na_ nb_ nc_ nd_ l3 H_Qhomographic_sg_denom_nonzero); intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = (l1, (0%Z, (na_, (0%Z, nb_)), (0%Z, (nc_, (0%Z, nd_))), (l3, One)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h (dL xs) One H_Qquadratic_sg_denom_nonzero); [ apply sym_eq; assumption | apply H1; fold L3 in |- *; repeat (apply pair_2; try reflexivity); discriminate || reflexivity ] | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end; repeat rewrite ZERO_left; repeat rewrite Zplus_0_r ]; apply (sg_neg_1 (a + b) (c + d) (e + f) (g + h) (dL xs) H_Qhomographic_sg_denom_nonzero na_ nb_ nc_ nd_ l3); rewrite hl; fold L3 in |- *; repeat (apply pair_2; try reflexivity); discriminate || reflexivity. generalize (Qquadratic_signok_0 _ _ _ _ _ H_Qquadratic_sg_denom_nonzero). intros H_Qhomographic_sg_denom_nonzero. set (L3 := Qhomographic_sign (a + c) (b + d) (e + g) (f + h) p2 H_Qhomographic_sg_denom_nonzero) in *. set (l1 := fst L3) in *. set (l2 := fst (snd L3)) in *. set (l3 := snd (snd L3)) in *. set (na_ := fst l2) in *. set (nb_ := fst (snd l2)) in *. set (nc_ := fst (snd (snd l2))) in *. set (nd_ := snd (snd (snd l2))) in *. generalize (Qquadratic_sign_One_y a b c d e f g h One p2 H_Qquadratic_sg_denom_nonzero l1 na_ nb_ nc_ nd_ l3 H_Qhomographic_sg_denom_nonzero); intros H1. assert (H_tuple_eq : ((-1)%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2))) = (l1, (0%Z, (0%Z, (na_, nb_)), (0%Z, (0%Z, (nc_, nd_))), (One, l3)))); [ apply trans_eq with (Qquadratic_sign a b c d e f g h One p2 H_Qquadratic_sg_denom_nonzero); [ apply sym_eq; assumption | apply H1; fold L3 in |- *; repeat (apply pair_2; try reflexivity); discriminate || reflexivity ] | generalize (Qquadratic_sign_tuple_equal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H_tuple_eq); intros (hl, ((hna, (hnb, (hnc, (hnd, (hne, (hnf, (hng, hnh))))))), (hp1, hp2))); do 10 match goal with | id1:(?X1 = ?X2) |- ?X3 => try rewrite id1; clear id1 end; repeat rewrite ZERO_left; repeat rewrite Zplus_0_r ]; apply (sg_neg_1 (a + c) (b + d) (e + g) (f + h) p2 H_Qhomographic_sg_denom_nonzero na_ nb_ nc_ nd_ l3); rewrite hl; fold L3 in |- *; repeat (apply pair_2; try reflexivity); discriminate || reflexivity. Qed.
imports: Coq(ZArithRing)