proposition: Lemma quadratic_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), q_sign a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero = Qsgn (spec_Qquadratic_Qpositive_to_Q a b c d e f g h p1 p2).
proof: Proof. fix quadratic_sign 9. intros a b c d e f g h. unfold q_sign in |- *. set (o1 := outside_square a b c d) in *. set (o2 := outside_square e f g h) in *. intros [xs| xs| ]. intros [ys| ys| ] H_Qquadratic_sg_denom_nonzero. case (three_integers_dec_inf b c d). intros (Hb, (Hc, Hd)). case (three_integers_dec_inf f g h). clear o1 o2 quadratic_sign; intros (Hf, (Hg, Hh)); rewrite (Qquadratic_sign_nRdL_nRdL_1 a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption)); subst; unfold spec_Qquadratic_Qpositive_to_Q in |- *; simpl in |- *; transitivity (Qsgn (Qmult (Qmult (Qmult a (Qpos (nR xs))) (Qpos (nR ys))) (Qinv (Qmult (Qmult e (Qpos (nR xs))) (Qpos (nR ys)))))); [ idtac | apply f_equal with Q; apply f_equal2 with Q Q; [ idtac | apply f_equal with Q ]; abstract ring ]; rewrite Qsgn_15; rewrite Qsgn_28; repeat rewrite Qsgn_15; simpl in |- *; do 2 rewrite Qsgn_29; abstract ring. case (Z_lt_dec 2 o2). clear quadratic_sign; intros H_o2_gt_2 Hfgh'; rewrite (Qquadratic_sign_nRdL_nRdL_2 a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption)); subst; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite (Qsgn_7 _ (outside_square_correct_1 _ _ _ _ (nR xs) (nR ys) H_o2_gt_2 Hfgh')) ; clear o1 o2 H_o2_gt_2; replace (Qplus (Qplus (Qplus (Qmult (Qmult a (Qpos (nR xs))) (Qpos (nR ys))) (Qmult 0%Z (Qpos (nR xs)))) (Qmult 0%Z (Qpos (nR ys)))) 0%Z) with (Qmult (Qmult a (Qpos (nR xs))) (Qpos (nR ys))); [ idtac | simpl; ring ]; repeat rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; abstract ring. case (Z_lt_dec o2 (-2)). clear quadratic_sign; intros H_o2_lt_min_2 H_o2_gt_2' Hfgh'; rewrite (Qquadratic_sign_nRdL_nRdL_3 a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption)); subst; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite (Qsgn_8 _ (outside_square_correct_2 _ _ _ _ (nR xs) (nR ys) H_o2_lt_min_2 Hfgh')); clear o1 o2 H_o2_lt_min_2 H_o2_gt_2'; replace (Qplus (Qplus (Qplus (Qmult (Qmult a (Qpos (nR xs))) (Qpos (nR ys))) (Qmult 0%Z (Qpos (nR xs)))) (Qmult 0%Z (Qpos (nR ys)))) 0%Z) with (Qmult (Qmult a (Qpos (nR xs))) (Qpos (nR ys))); [ idtac | simpl; ring ]; repeat rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; abstract ring. intros H_o2_lt_min_2' H_o2_gt_2' Hfgh'; rewrite (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 (nR xs)) (refl_equal (nR ys))) ; discriminate || (try (repeat split; assumption)); rewrite spec_Qquadratic_Qpositive_to_Q_nR_nR; rewrite <- (quadratic_sign 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)) ; reflexivity. intro Hbcd'. case (three_integers_dec_inf f g h). intros (Hf, (Hg, Hh)). case (Z_lt_dec 2 o1). clear quadratic_sign; intros H_o1_gt_2; rewrite (Qquadratic_sign_nRdL_nRdL_5 a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption)); subst; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite (Qsgn_7 _ (outside_square_correct_1 _ _ _ _ (nR xs) (nR ys) H_o1_gt_2 Hbcd')); clear o1 o2 H_o1_gt_2; replace (Qplus (Qplus (Qplus (Qmult (Qmult e (Qpos (nR xs))) (Qpos (nR ys))) (Qmult 0%Z (Qpos (nR xs)))) (Qmult 0%Z (Qpos (nR ys)))) 0%Z) with (Qmult (Qmult e (Qpos (nR xs))) (Qpos (nR ys))); [ idtac | simpl; ring ]; repeat rewrite Qsgn_15; rewrite Qsgn_29; unfold Qsgn in |- *; abstract ring. case (Z_lt_dec o1 (-2)). clear quadratic_sign; intros H_o1_lt_min_2 H_o1_gt_2'; rewrite (Qquadratic_sign_nRdL_nRdL_6 a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption)); subst; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite (Qsgn_8 _ (outside_square_correct_2 _ _ _ _ (nR xs) (nR ys) H_o1_lt_min_2 Hbcd')); clear o1 o2 H_o1_gt_2' H_o1_lt_min_2; replace (Qplus (Qplus (Qplus (Qmult (Qmult e (Qpos (nR xs))) (Qpos (nR ys))) (Qmult 0%Z (Qpos (nR xs)))) (Qmult 0%Z (Qpos (nR ys)))) 0%Z) with (Qmult (Qmult e (Qpos (nR xs))) (Qpos (nR ys))); [ idtac | simpl; ring ]; repeat rewrite Qsgn_15; rewrite Qsgn_29; unfold Qsgn in |- *; abstract ring. intros H_o1_lt_min_2' H_o1_gt_2'; rewrite (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 (nR xs)) (refl_equal (nR ys))) ; discriminate || (try (repeat split; assumption)); rewrite spec_Qquadratic_Qpositive_to_Q_nR_nR; rewrite <- (quadratic_sign 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)); reflexivity. intro Hfgh'. case (inside_square_1_dec_inf o1 o2). clear quadratic_sign; intro H_inside_1; (rewrite (Qquadratic_sign_nRdL_nRdL_8 a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption))); generalize H_inside_1; intros [(H_o1, H_o2)| (H_o1, H_o2)]; Inside_Square_Qsgn_ (nR xs) (nR ys); intros H_num H_denom; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite H_num; rewrite H_denom; constructor. intro H_inside_1'. case (inside_square_2_dec_inf o1 o2). clear quadratic_sign; intro H_inside_2; (rewrite (Qquadratic_sign_nRdL_nRdL_9 a b c d e f g h (nR xs) (nR ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption))); generalize H_inside_2; intros [(H_o1, H_o2)| (H_o1, H_o2)]; Inside_Square_Qsgn_ (nR xs) (nR ys); intros H_num H_denom; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite H_num; rewrite H_denom; constructor. intros H_inside_2'. rewrite (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 (nR xs)) (refl_equal (nR ys))) ; discriminate || (try (repeat split; assumption)); rewrite spec_Qquadratic_Qpositive_to_Q_nR_nR; rewrite <- (quadratic_sign 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)); reflexivity. case (three_integers_dec_inf b c d). intros (Hb, (Hc, Hd)). case (three_integers_dec_inf f g h). clear o1 o2 quadratic_sign; intros (Hf, (Hg, Hh)); rewrite (Qquadratic_sign_nRdL_nRdL_1 a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption)); subst; unfold spec_Qquadratic_Qpositive_to_Q in |- *; simpl in |- *; transitivity (Qsgn (Qmult (Qmult (Qmult a (Qpos (nR xs))) (Qpos (dL ys))) (Qinv (Qmult (Qmult e (Qpos (nR xs))) (Qpos (dL ys)))))); [ idtac | apply f_equal with Q; apply f_equal2 with Q Q; [ idtac | apply f_equal with Q ]; abstract ring ]; rewrite Qsgn_15; rewrite Qsgn_28; repeat rewrite Qsgn_15; simpl in |- *; do 2 rewrite Qsgn_29; abstract ring. case (Z_lt_dec 2 o2). clear quadratic_sign; intros H_o2_gt_2 Hfgh'; rewrite (Qquadratic_sign_nRdL_nRdL_2 a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption)); subst; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite (Qsgn_7 _ (outside_square_correct_1 _ _ _ _ (nR xs) (dL ys) H_o2_gt_2 Hfgh')) ; clear o1 o2 H_o2_gt_2; replace (Qplus (Qplus (Qplus (Qmult (Qmult a (Qpos (nR xs))) (Qpos (dL ys))) (Qmult 0%Z (Qpos (nR xs)))) (Qmult 0%Z (Qpos (dL ys)))) 0%Z) with (Qmult (Qmult a (Qpos (nR xs))) (Qpos (dL ys))); [ idtac | simpl; ring ]; repeat rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; abstract ring. case (Z_lt_dec o2 (-2)). clear quadratic_sign; intros H_o2_lt_min_2 H_o2_gt_2' Hfgh'; rewrite (Qquadratic_sign_nRdL_nRdL_3 a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption)); subst; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite (Qsgn_8 _ (outside_square_correct_2 _ _ _ _ (nR xs) (dL ys) H_o2_lt_min_2 Hfgh')); clear o1 o2 H_o2_lt_min_2 H_o2_gt_2'; replace (Qplus (Qplus (Qplus (Qmult (Qmult a (Qpos (nR xs))) (Qpos (dL ys))) (Qmult 0%Z (Qpos (nR xs)))) (Qmult 0%Z (Qpos (dL ys)))) 0%Z) with (Qmult (Qmult a (Qpos (nR xs))) (Qpos (dL ys))); [ idtac | simpl; ring ]; repeat rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; abstract ring. intros H_o2_lt_min_2' H_o2_gt_2' Hfgh'; rewrite (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 (nR xs)) (refl_equal (dL ys))) ; discriminate || (try (repeat split; assumption)); rewrite spec_Qquadratic_Qpositive_to_Q_nR_dL; rewrite <- (quadratic_sign (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)) ; reflexivity. intro Hbcd'. case (three_integers_dec_inf f g h). intros (Hf, (Hg, Hh)). case (Z_lt_dec 2 o1). clear quadratic_sign; intros H_o1_gt_2; rewrite (Qquadratic_sign_nRdL_nRdL_5 a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption)); subst; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite (Qsgn_7 _ (outside_square_correct_1 _ _ _ _ (nR xs) (dL ys) H_o1_gt_2 Hbcd')); clear o1 o2 H_o1_gt_2; replace (Qplus (Qplus (Qplus (Qmult (Qmult e (Qpos (nR xs))) (Qpos (dL ys))) (Qmult 0%Z (Qpos (nR xs)))) (Qmult 0%Z (Qpos (dL ys)))) 0%Z) with (Qmult (Qmult e (Qpos (nR xs))) (Qpos (dL ys))); [ idtac | simpl; ring ]; repeat rewrite Qsgn_15; rewrite Qsgn_29; unfold Qsgn in |- *; ring. case (Z_lt_dec o1 (-2)). clear quadratic_sign; intros H_o1_lt_min_2 H_o1_gt_2'; rewrite (Qquadratic_sign_nRdL_nRdL_6 a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption)); subst; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite (Qsgn_8 _ (outside_square_correct_2 _ _ _ _ (nR xs) (dL ys) H_o1_lt_min_2 Hbcd')); clear o1 o2 H_o1_gt_2' H_o1_lt_min_2; replace (Qplus (Qplus (Qplus (Qmult (Qmult e (Qpos (nR xs))) (Qpos (dL ys))) (Qmult 0%Z (Qpos (nR xs)))) (Qmult 0%Z (Qpos (dL ys)))) 0%Z) with (Qmult (Qmult e (Qpos (nR xs))) (Qpos (dL ys))); [ idtac | simpl; ring ]; repeat rewrite Qsgn_15; rewrite Qsgn_29; unfold Qsgn in |- *; ring. intros H_o1_lt_min_2' H_o1_gt_2'; rewrite (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 (nR xs)) (refl_equal (dL ys))) ; discriminate || (try (repeat split; assumption)); rewrite spec_Qquadratic_Qpositive_to_Q_nR_dL; rewrite <- (quadratic_sign (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)); reflexivity. intro Hfgh'. case (inside_square_1_dec_inf o1 o2). clear quadratic_sign; intro H_inside_1; (rewrite (Qquadratic_sign_nRdL_nRdL_8 a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption))); generalize H_inside_1; intros [(H_o1, H_o2)| (H_o1, H_o2)]; Inside_Square_Qsgn_ (nR xs) (dL ys); intros H_num H_denom; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite H_num; rewrite H_denom; constructor. intro H_inside_1'. case (inside_square_2_dec_inf o1 o2). clear quadratic_sign; intro H_inside_2; (rewrite (Qquadratic_sign_nRdL_nRdL_9 a b c d e f g h (nR xs) (dL ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption))); generalize H_inside_2; intros [(H_o1, H_o2)| (H_o1, H_o2)]; Inside_Square_Qsgn_ (nR xs) (dL ys); intros H_num H_denom; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite H_num; rewrite H_denom; constructor. intros H_inside_2'. rewrite (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 (nR xs)) (refl_equal (dL ys))) ; discriminate || (try (repeat split; assumption)); rewrite spec_Qquadratic_Qpositive_to_Q_nR_dL; rewrite <- (quadratic_sign (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)); reflexivity. clear quadratic_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 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 *. rewrite (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); [ idtac | fold L3 in |- *; repeat (apply pair_2; try reflexivity) | discriminate | reflexivity ]. rewrite spec_Qquadratic_Qpositive_to_Q_p_One. rewrite <- (homographic_sign (a + b) (c + d) (e + f) (g + h) (nR xs) H_Qhomographic_sg_denom_nonzero). reflexivity. intros [ys| ys| ] H_Qquadratic_sg_denom_nonzero. case (three_integers_dec_inf b c d). intros (Hb, (Hc, Hd)). case (three_integers_dec_inf f g h). clear o1 o2 quadratic_sign; intros (Hf, (Hg, Hh)); rewrite (Qquadratic_sign_nRdL_nRdL_1 a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption)); subst; unfold spec_Qquadratic_Qpositive_to_Q in |- *; simpl in |- *; transitivity (Qsgn (Qmult (Qmult (Qmult a (Qpos (dL xs))) (Qpos (nR ys))) (Qinv (Qmult (Qmult e (Qpos (dL xs))) (Qpos (nR ys)))))); [ idtac | apply f_equal with Q; apply f_equal2 with Q Q; [ idtac | apply f_equal with Q ]; simpl; ring ]; rewrite Qsgn_15; rewrite Qsgn_28; repeat rewrite Qsgn_15; simpl in |- *; do 2 rewrite Qsgn_29; ring. case (Z_lt_dec 2 o2). clear quadratic_sign; intros H_o2_gt_2 Hfgh'; rewrite (Qquadratic_sign_nRdL_nRdL_2 a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption)); subst; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite (Qsgn_7 _ (outside_square_correct_1 _ _ _ _ (dL xs) (nR ys) H_o2_gt_2 Hfgh')) ; clear o1 o2 H_o2_gt_2; replace (Qplus (Qplus (Qplus (Qmult (Qmult a (Qpos (dL xs))) (Qpos (nR ys))) (Qmult 0%Z (Qpos (dL xs)))) (Qmult 0%Z (Qpos (nR ys)))) 0%Z) with (Qmult (Qmult a (Qpos (dL xs))) (Qpos (nR ys))); [ idtac | simpl; ring ]; repeat rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; ring. case (Z_lt_dec o2 (-2)). clear quadratic_sign; intros H_o2_lt_min_2 H_o2_gt_2' Hfgh'; rewrite (Qquadratic_sign_nRdL_nRdL_3 a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption)); subst; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite (Qsgn_8 _ (outside_square_correct_2 _ _ _ _ (dL xs) (nR ys) H_o2_lt_min_2 Hfgh')); clear o1 o2 H_o2_lt_min_2 H_o2_gt_2'; replace (Qplus (Qplus (Qplus (Qmult (Qmult a (Qpos (dL xs))) (Qpos (nR ys))) (Qmult 0%Z (Qpos (dL xs)))) (Qmult 0%Z (Qpos (nR ys)))) 0%Z) with (Qmult (Qmult a (Qpos (dL xs))) (Qpos (nR ys))); [ idtac | simpl; ring ]; repeat rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; ring. intros H_o2_lt_min_2' H_o2_gt_2' Hfgh'; rewrite (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 (dL xs)) (refl_equal (nR ys))) ; discriminate || (try (repeat split; assumption)); rewrite spec_Qquadratic_Qpositive_to_Q_dL_nR; rewrite <- (quadratic_sign (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)) ; reflexivity. intro Hbcd'. case (three_integers_dec_inf f g h). intros (Hf, (Hg, Hh)). case (Z_lt_dec 2 o1). clear quadratic_sign; intros H_o1_gt_2; rewrite (Qquadratic_sign_nRdL_nRdL_5 a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption)); subst; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite (Qsgn_7 _ (outside_square_correct_1 _ _ _ _ (dL xs) (nR ys) H_o1_gt_2 Hbcd')); clear o1 o2 H_o1_gt_2; replace (Qplus (Qplus (Qplus (Qmult (Qmult e (Qpos (dL xs))) (Qpos (nR ys))) (Qmult 0%Z (Qpos (dL xs)))) (Qmult 0%Z (Qpos (nR ys)))) 0%Z) with (Qmult (Qmult e (Qpos (dL xs))) (Qpos (nR ys))); [ idtac | simpl; ring ]; repeat rewrite Qsgn_15; rewrite Qsgn_29; unfold Qsgn in |- *; ring. case (Z_lt_dec o1 (-2)). clear quadratic_sign; intros H_o1_lt_min_2 H_o1_gt_2'; rewrite (Qquadratic_sign_nRdL_nRdL_6 a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption)); subst; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite (Qsgn_8 _ (outside_square_correct_2 _ _ _ _ (dL xs) (nR ys) H_o1_lt_min_2 Hbcd')); clear o1 o2 H_o1_gt_2' H_o1_lt_min_2; replace (Qplus (Qplus (Qplus (Qmult (Qmult e (Qpos (dL xs))) (Qpos (nR ys))) (Qmult 0%Z (Qpos (dL xs)))) (Qmult 0%Z (Qpos (nR ys)))) 0%Z) with (Qmult (Qmult e (Qpos (dL xs))) (Qpos (nR ys))); [ idtac | simpl; ring ]; repeat rewrite Qsgn_15; rewrite Qsgn_29; unfold Qsgn in |- *; ring. intros H_o1_lt_min_2' H_o1_gt_2'; rewrite (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 (dL xs)) (refl_equal (nR ys))) ; discriminate || (try (repeat split; assumption)); rewrite spec_Qquadratic_Qpositive_to_Q_dL_nR; rewrite <- (quadratic_sign (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)); reflexivity. intro Hfgh'. case (inside_square_1_dec_inf o1 o2). clear quadratic_sign; intro H_inside_1; (rewrite (Qquadratic_sign_nRdL_nRdL_8 a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption))); generalize H_inside_1; intros [(H_o1, H_o2)| (H_o1, H_o2)]; Inside_Square_Qsgn_ (dL xs) (nR ys); intros H_num H_denom; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite H_num; rewrite H_denom; constructor. intro H_inside_1'. case (inside_square_2_dec_inf o1 o2). clear quadratic_sign; intro H_inside_2; (rewrite (Qquadratic_sign_nRdL_nRdL_9 a b c d e f g h (dL xs) (nR ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption))); generalize H_inside_2; intros [(H_o1, H_o2)| (H_o1, H_o2)]; Inside_Square_Qsgn_ (dL xs) (nR ys); intros H_num H_denom; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite H_num; rewrite H_denom; constructor. intros H_inside_2'. rewrite (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 (dL xs)) (refl_equal (nR ys))) ; discriminate || (try (repeat split; assumption)); rewrite spec_Qquadratic_Qpositive_to_Q_dL_nR; rewrite <- (quadratic_sign (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)); reflexivity. case (three_integers_dec_inf b c d). intros (Hb, (Hc, Hd)). case (three_integers_dec_inf f g h). clear o1 o2 quadratic_sign; intros (Hf, (Hg, Hh)); rewrite (Qquadratic_sign_nRdL_nRdL_1 a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption)); subst; unfold spec_Qquadratic_Qpositive_to_Q in |- *; simpl in |- *; transitivity (Qsgn (Qmult (Qmult (Qmult a (Qpos (dL xs))) (Qpos (dL ys))) (Qinv (Qmult (Qmult e (Qpos (dL xs))) (Qpos (dL ys)))))); [ idtac | apply f_equal with Q; apply f_equal2 with Q Q; [ idtac | apply f_equal with Q ]; simpl; ring ]; rewrite Qsgn_15; rewrite Qsgn_28; repeat rewrite Qsgn_15; simpl in |- *; do 2 rewrite Qsgn_29; ring. case (Z_lt_dec 2 o2). clear quadratic_sign; intros H_o2_gt_2 Hfgh'; rewrite (Qquadratic_sign_nRdL_nRdL_2 a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption)); subst; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite (Qsgn_7 _ (outside_square_correct_1 _ _ _ _ (dL xs) (dL ys) H_o2_gt_2 Hfgh')) ; clear o1 o2 H_o2_gt_2; replace (Qplus (Qplus (Qplus (Qmult (Qmult a (Qpos (dL xs))) (Qpos (dL ys))) (Qmult 0%Z (Qpos (dL xs)))) (Qmult 0%Z (Qpos (dL ys)))) 0%Z) with (Qmult (Qmult a (Qpos (dL xs))) (Qpos (dL ys))); [ idtac | simpl; ring ]; repeat rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; ring. case (Z_lt_dec o2 (-2)). clear quadratic_sign; intros H_o2_lt_min_2 H_o2_gt_2' Hfgh'; rewrite (Qquadratic_sign_nRdL_nRdL_3 a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption)); subst; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite (Qsgn_8 _ (outside_square_correct_2 _ _ _ _ (dL xs) (dL ys) H_o2_lt_min_2 Hfgh')); clear o1 o2 H_o2_lt_min_2 H_o2_gt_2'; replace (Qplus (Qplus (Qplus (Qmult (Qmult a (Qpos (dL xs))) (Qpos (dL ys))) (Qmult 0%Z (Qpos (dL xs)))) (Qmult 0%Z (Qpos (dL ys)))) 0%Z) with (Qmult (Qmult a (Qpos (dL xs))) (Qpos (dL ys))); [ idtac | simpl; ring ]; repeat rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; ring. intros H_o2_lt_min_2' H_o2_gt_2' Hfgh'; rewrite (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 (dL xs)) (refl_equal (dL ys))) ; discriminate || (try (repeat split; assumption)); rewrite spec_Qquadratic_Qpositive_to_Q_dL_dL; rewrite <- (quadratic_sign (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)) ; reflexivity. intro Hbcd'. case (three_integers_dec_inf f g h). intros (Hf, (Hg, Hh)). case (Z_lt_dec 2 o1). clear quadratic_sign; intros H_o1_gt_2; rewrite (Qquadratic_sign_nRdL_nRdL_5 a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption)); subst; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite (Qsgn_7 _ (outside_square_correct_1 _ _ _ _ (dL xs) (dL ys) H_o1_gt_2 Hbcd')); clear o1 o2 H_o1_gt_2; replace (Qplus (Qplus (Qplus (Qmult (Qmult e (Qpos (dL xs))) (Qpos (dL ys))) (Qmult 0%Z (Qpos (dL xs)))) (Qmult 0%Z (Qpos (dL ys)))) 0%Z) with (Qmult (Qmult e (Qpos (dL xs))) (Qpos (dL ys))); [ idtac | simpl; ring ]; repeat rewrite Qsgn_15; rewrite Qsgn_29; unfold Qsgn in |- *; ring. case (Z_lt_dec o1 (-2)). clear quadratic_sign; intros H_o1_lt_min_2 H_o1_gt_2'; rewrite (Qquadratic_sign_nRdL_nRdL_6 a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption)); subst; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite (Qsgn_8 _ (outside_square_correct_2 _ _ _ _ (dL xs) (dL ys) H_o1_lt_min_2 Hbcd')); clear o1 o2 H_o1_gt_2' H_o1_lt_min_2; replace (Qplus (Qplus (Qplus (Qmult (Qmult e (Qpos (dL xs))) (Qpos (dL ys))) (Qmult 0%Z (Qpos (dL xs)))) (Qmult 0%Z (Qpos (dL ys)))) 0%Z) with (Qmult (Qmult e (Qpos (dL xs))) (Qpos (dL ys))); [ idtac | simpl; ring ]; repeat rewrite Qsgn_15; rewrite Qsgn_29; unfold Qsgn in |- *; ring. intros H_o1_lt_min_2' H_o1_gt_2'; rewrite (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 (dL xs)) (refl_equal (dL ys))) ; discriminate || (try (repeat split; assumption)); rewrite spec_Qquadratic_Qpositive_to_Q_dL_dL; rewrite <- (quadratic_sign (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)); reflexivity. intro Hfgh'. case (inside_square_1_dec_inf o1 o2). clear quadratic_sign; intro H_inside_1; (rewrite (Qquadratic_sign_nRdL_nRdL_8 a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption))); generalize H_inside_1; intros [(H_o1, H_o2)| (H_o1, H_o2)]; Inside_Square_Qsgn_ (dL xs) (dL ys); intros H_num H_denom; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite H_num; rewrite H_denom; constructor. intro H_inside_1'. case (inside_square_2_dec_inf o1 o2). clear quadratic_sign; intro H_inside_2; (rewrite (Qquadratic_sign_nRdL_nRdL_9 a b c d e f g h (dL xs) (dL ys) H_Qquadratic_sg_denom_nonzero) ; discriminate || (try (repeat split; assumption))); generalize H_inside_2; intros [(H_o1, H_o2)| (H_o1, H_o2)]; Inside_Square_Qsgn_ (dL xs) (dL ys); intros H_num H_denom; unfold spec_Qquadratic_Qpositive_to_Q in |- *; rewrite Qsgn_15; rewrite Qsgn_28; rewrite H_num; rewrite H_denom; constructor. intros H_inside_2'. rewrite (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 (dL xs)) (refl_equal (dL ys))) ; discriminate || (try (repeat split; assumption)); rewrite spec_Qquadratic_Qpositive_to_Q_dL_dL; rewrite <- (quadratic_sign (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)); reflexivity. clear quadratic_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 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 *. rewrite (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); [ idtac | fold L3 in |- *; repeat (apply pair_2; try reflexivity) | discriminate | reflexivity ]. rewrite spec_Qquadratic_Qpositive_to_Q_p_One. rewrite <- (homographic_sign (a + b) (c + d) (e + f) (g + h) (dL xs) H_Qhomographic_sg_denom_nonzero). reflexivity. intros p2 H_Qquadratic_sg_denom_nonzero; clear quadratic_sign. 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); [ idtac | fold L3 in |- *; repeat (apply pair_2; try reflexivity) | reflexivity ]. rewrite spec_Qquadratic_Qpositive_to_Q_One_p. rewrite <- (homographic_sign (a + c) (b + d) (e + g) (f + h) p2 H_Qhomographic_sg_denom_nonzero). reflexivity. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)