proposition: Lemma Qquadratic_sign_sign : 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), let (l1, L2) := Qquadratic_sign a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero in {l1 = 0%Z} + {l1 = 1%Z} + {l1 = (-1)%Z}.
proof: Proof. fix Qquadratic_sign_sign 9. intros. destruct p1 as [p| p| ]. destruct p2 as [p0| p0| ]. case (three_integers_dec_inf b c d); intro Hbcd; case (three_integers_dec_inf f g h); intro Hfgh; [ rewrite Qquadratic_sign_nRdL_nRdL_1; try solve [ discriminate | assumption ]; rewrite <- Zsgn_15; apply Zsgn_1' | case (Z_lt_dec 2 (outside_square e f g h)); intro Ho2; [ rewrite Qquadratic_sign_nRdL_nRdL_2; try solve [ discriminate | assumption ]; apply Zsgn_1' | case (Z_lt_dec (outside_square e f g h) (-2)); intro Ho2'; [ rewrite Qquadratic_sign_nRdL_nRdL_3; try solve [ discriminate | assumption ]; rewrite <- Zsgn_25; apply Zsgn_1' | match goal with | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_nR_4 a b c d e f g h (nR p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_1 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho2 Ho2') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_dL_4 a b c d e f g h (nR p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_2 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho2 Ho2') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_nR_4 a b c d e f g h (dL p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_3 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho2 Ho2') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_dL_4 a b c d e f g h (dL p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_4 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho2 Ho2') end; apply Qquadratic_sign_sign ] ] | case (Z_lt_dec 2 (outside_square a b c d)); intro Ho1; [ rewrite Qquadratic_sign_nRdL_nRdL_5; try solve [ discriminate | assumption ]; apply Zsgn_1' | case (Z_lt_dec (outside_square a b c d) (-2)); intro Ho1'; [ rewrite Qquadratic_sign_nRdL_nRdL_6; try solve [ discriminate | assumption ]; rewrite <- Zsgn_25; apply Zsgn_1' | match goal with | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_nR_7 a b c d e f g h (nR p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_1 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho1 Ho1') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_dL_7 a b c d e f g h (nR p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_2 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho1 Ho1') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_nR_7 a b c d e f g h (dL p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_3 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho1 Ho1') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_dL_7 a b c d e f g h (dL p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_4 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho1 Ho1') end; apply Qquadratic_sign_sign ] ] | case (inside_square_1_dec_inf (outside_square a b c d) (outside_square e f g h)); intro H_inside_1; [ rewrite Qquadratic_sign_nRdL_nRdL_8; try solve [ discriminate | assumption ]; left; right; reflexivity | case (inside_square_2_dec_inf (outside_square a b c d) (outside_square e f g h)); intro H_inside_2; [ rewrite Qquadratic_sign_nRdL_nRdL_9; try solve [ discriminate | assumption ]; right; reflexivity | match goal with | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_nR_10 a b c d e f g h (nR p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_1 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh H_inside_1 H_inside_2) | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_dL_10 a b c d e f g h (nR p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_2 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh H_inside_1 H_inside_2) | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_nR_10 a b c d e f g h (dL p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_3 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh H_inside_1 H_inside_2) | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_dL_10 a b c d e f g h (dL p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_4 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh H_inside_1 H_inside_2) end; apply Qquadratic_sign_sign ] ] ]. case (three_integers_dec_inf b c d); intro Hbcd; case (three_integers_dec_inf f g h); intro Hfgh; [ rewrite Qquadratic_sign_nRdL_nRdL_1; try solve [ discriminate | assumption ]; rewrite <- Zsgn_15; apply Zsgn_1' | case (Z_lt_dec 2 (outside_square e f g h)); intro Ho2; [ rewrite Qquadratic_sign_nRdL_nRdL_2; try solve [ discriminate | assumption ]; apply Zsgn_1' | case (Z_lt_dec (outside_square e f g h) (-2)); intro Ho2'; [ rewrite Qquadratic_sign_nRdL_nRdL_3; try solve [ discriminate | assumption ]; rewrite <- Zsgn_25; apply Zsgn_1' | match goal with | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_nR_4 a b c d e f g h (nR p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_1 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho2 Ho2') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_dL_4 a b c d e f g h (nR p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_2 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho2 Ho2') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_nR_4 a b c d e f g h (dL p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_3 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho2 Ho2') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_dL_4 a b c d e f g h (dL p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_4 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho2 Ho2') end; apply Qquadratic_sign_sign ] ] | case (Z_lt_dec 2 (outside_square a b c d)); intro Ho1; [ rewrite Qquadratic_sign_nRdL_nRdL_5; try solve [ discriminate | assumption ]; apply Zsgn_1' | case (Z_lt_dec (outside_square a b c d) (-2)); intro Ho1'; [ rewrite Qquadratic_sign_nRdL_nRdL_6; try solve [ discriminate | assumption ]; rewrite <- Zsgn_25; apply Zsgn_1' | match goal with | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_nR_7 a b c d e f g h (nR p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_1 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho1 Ho1') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_dL_7 a b c d e f g h (nR p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_2 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho1 Ho1') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_nR_7 a b c d e f g h (dL p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_3 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho1 Ho1') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_dL_7 a b c d e f g h (dL p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_4 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho1 Ho1') end; apply Qquadratic_sign_sign ] ] | case (inside_square_1_dec_inf (outside_square a b c d) (outside_square e f g h)); intro H_inside_1; [ rewrite Qquadratic_sign_nRdL_nRdL_8; try solve [ discriminate | assumption ]; left; right; reflexivity | case (inside_square_2_dec_inf (outside_square a b c d) (outside_square e f g h)); intro H_inside_2; [ rewrite Qquadratic_sign_nRdL_nRdL_9; try solve [ discriminate | assumption ]; right; reflexivity | match goal with | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_nR_10 a b c d e f g h (nR p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_1 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh H_inside_1 H_inside_2) | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_dL_10 a b c d e f g h (nR p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_2 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh H_inside_1 H_inside_2) | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_nR_10 a b c d e f g h (dL p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_3 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh H_inside_1 H_inside_2) | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_dL_10 a b c d e f g h (dL p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_4 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh H_inside_1 H_inside_2) end; apply Qquadratic_sign_sign ] ] ]. generalize (Qquadratic_signok_0' _ _ _ _ _ H_Qquadratic_sg_denom_nonzero); intro H_Qhomographic_sg_denom_nonzero; set (L3 := Qhomographic_sign (a + b) (c + d) (e + f) (g + h) (nR p) 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 *; rewrite (Qquadratic_sign_nRdL_One a b c d e f g h (nR p) One H_Qquadratic_sg_denom_nonzero l1' na nb nc nd l3 H_Qhomographic_sg_denom_nonzero); [ replace l1' with (h_sign (a + b) (c + d) (e + f) (g + h) (nR p) H_Qhomographic_sg_denom_nonzero); [ apply sg_sign_dec | reflexivity ] | fold L3 in |- *; repeat (apply pair_2; try reflexivity); discriminate || reflexivity | discriminate | reflexivity ]. destruct p2 as [p0| p0| ]. case (three_integers_dec_inf b c d); intro Hbcd; case (three_integers_dec_inf f g h); intro Hfgh; [ rewrite Qquadratic_sign_nRdL_nRdL_1; try solve [ discriminate | assumption ]; rewrite <- Zsgn_15; apply Zsgn_1' | case (Z_lt_dec 2 (outside_square e f g h)); intro Ho2; [ rewrite Qquadratic_sign_nRdL_nRdL_2; try solve [ discriminate | assumption ]; apply Zsgn_1' | case (Z_lt_dec (outside_square e f g h) (-2)); intro Ho2'; [ rewrite Qquadratic_sign_nRdL_nRdL_3; try solve [ discriminate | assumption ]; rewrite <- Zsgn_25; apply Zsgn_1' | match goal with | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_nR_4 a b c d e f g h (nR p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_1 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho2 Ho2') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_dL_4 a b c d e f g h (nR p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_2 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho2 Ho2') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_nR_4 a b c d e f g h (dL p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_3 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho2 Ho2') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_dL_4 a b c d e f g h (dL p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_4 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho2 Ho2') end; apply Qquadratic_sign_sign ] ] | case (Z_lt_dec 2 (outside_square a b c d)); intro Ho1; [ rewrite Qquadratic_sign_nRdL_nRdL_5; try solve [ discriminate | assumption ]; apply Zsgn_1' | case (Z_lt_dec (outside_square a b c d) (-2)); intro Ho1'; [ rewrite Qquadratic_sign_nRdL_nRdL_6; try solve [ discriminate | assumption ]; rewrite <- Zsgn_25; apply Zsgn_1' | match goal with | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_nR_7 a b c d e f g h (nR p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_1 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho1 Ho1') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_dL_7 a b c d e f g h (nR p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_2 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho1 Ho1') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_nR_7 a b c d e f g h (dL p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_3 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho1 Ho1') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_dL_7 a b c d e f g h (dL p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_4 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho1 Ho1') end; apply Qquadratic_sign_sign ] ] | case (inside_square_1_dec_inf (outside_square a b c d) (outside_square e f g h)); intro H_inside_1; [ rewrite Qquadratic_sign_nRdL_nRdL_8; try solve [ discriminate | assumption ]; left; right; reflexivity | case (inside_square_2_dec_inf (outside_square a b c d) (outside_square e f g h)); intro H_inside_2; [ rewrite Qquadratic_sign_nRdL_nRdL_9; try solve [ discriminate | assumption ]; right; reflexivity | match goal with | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_nR_10 a b c d e f g h (nR p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_1 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh H_inside_1 H_inside_2) | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_dL_10 a b c d e f g h (nR p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_2 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh H_inside_1 H_inside_2) | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_nR_10 a b c d e f g h (dL p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_3 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh H_inside_1 H_inside_2) | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_dL_10 a b c d e f g h (dL p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_4 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh H_inside_1 H_inside_2) end; apply Qquadratic_sign_sign ] ] ]. case (three_integers_dec_inf b c d); intro Hbcd; case (three_integers_dec_inf f g h); intro Hfgh; [ rewrite Qquadratic_sign_nRdL_nRdL_1; try solve [ discriminate | assumption ]; rewrite <- Zsgn_15; apply Zsgn_1' | case (Z_lt_dec 2 (outside_square e f g h)); intro Ho2; [ rewrite Qquadratic_sign_nRdL_nRdL_2; try solve [ discriminate | assumption ]; apply Zsgn_1' | case (Z_lt_dec (outside_square e f g h) (-2)); intro Ho2'; [ rewrite Qquadratic_sign_nRdL_nRdL_3; try solve [ discriminate | assumption ]; rewrite <- Zsgn_25; apply Zsgn_1' | match goal with | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_nR_4 a b c d e f g h (nR p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_1 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho2 Ho2') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_dL_4 a b c d e f g h (nR p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_2 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho2 Ho2') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_nR_4 a b c d e f g h (dL p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_3 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho2 Ho2') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_dL_4 a b c d e f g h (dL p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_4 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho2 Ho2') end; apply Qquadratic_sign_sign ] ] | case (Z_lt_dec 2 (outside_square a b c d)); intro Ho1; [ rewrite Qquadratic_sign_nRdL_nRdL_5; try solve [ discriminate | assumption ]; apply Zsgn_1' | case (Z_lt_dec (outside_square a b c d) (-2)); intro Ho1'; [ rewrite Qquadratic_sign_nRdL_nRdL_6; try solve [ discriminate | assumption ]; rewrite <- Zsgn_25; apply Zsgn_1' | match goal with | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_nR_7 a b c d e f g h (nR p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_1 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho1 Ho1') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_dL_7 a b c d e f g h (nR p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_2 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho1 Ho1') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_nR_7 a b c d e f g h (dL p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_3 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho1 Ho1') | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_dL_7 a b c d e f g h (dL p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_4 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh Ho1 Ho1') end; apply Qquadratic_sign_sign ] ] | case (inside_square_1_dec_inf (outside_square a b c d) (outside_square e f g h)); intro H_inside_1; [ rewrite Qquadratic_sign_nRdL_nRdL_8; try solve [ discriminate | assumption ]; left; right; reflexivity | case (inside_square_2_dec_inf (outside_square a b c d) (outside_square e f g h)); intro H_inside_2; [ rewrite Qquadratic_sign_nRdL_nRdL_9; try solve [ discriminate | assumption ]; right; reflexivity | match goal with | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_nR_10 a b c d e f g h (nR p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_1 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh H_inside_1 H_inside_2) | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_nR_dL_10 a b c d e f g h (nR p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_2 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh H_inside_1 H_inside_2) | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (nR ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_nR_10 a b c d e f g h (dL p) p (nR p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_3 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh H_inside_1 H_inside_2) | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (dL ?X6) (dL ?X7)) |- ?X8 => rewrite (Qquadratic_sign_dL_dL_10 a b c d e f g h (dL p) p (dL p0) p0 H_Qquadratic_sg_denom_nonzero (Qquadratic_signok_4 e f g h p p0 H_Qquadratic_sg_denom_nonzero) (refl_equal _) (refl_equal _) Hbcd Hfgh H_inside_1 H_inside_2) end; apply Qquadratic_sign_sign ] ] ]. generalize (Qquadratic_signok_0' _ _ _ _ _ H_Qquadratic_sg_denom_nonzero); intro H_Qhomographic_sg_denom_nonzero; set (L3 := Qhomographic_sign (a + b) (c + d) (e + f) (g + h) (dL p) 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 *; rewrite (Qquadratic_sign_nRdL_One a b c d e f g h (dL p) One H_Qquadratic_sg_denom_nonzero l1' na nb nc nd l3 H_Qhomographic_sg_denom_nonzero); [ replace l1' with (h_sign (a + b) (c + d) (e + f) (g + h) (dL p) H_Qhomographic_sg_denom_nonzero); [ apply sg_sign_dec | reflexivity ] | fold L3 in |- *; repeat (apply pair_2; try reflexivity); discriminate || reflexivity | discriminate | reflexivity ]. generalize (Qquadratic_signok_0 _ _ _ _ _ H_Qquadratic_sg_denom_nonzero); intro 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 *; rewrite (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); [ replace l1' with (h_sign (a + c) (b + d) (e + g) (f + h) p2 H_Qhomographic_sg_denom_nonzero); [ apply sg_sign_dec | reflexivity ] | fold L3 in |- *; repeat (apply pair_2; try reflexivity); discriminate || reflexivity | reflexivity ]. Qed.
imports: Coq(ZArithRing) QArithSternBrocot(Qhomographic_sign) QArithSternBrocot(Zaux)