proposition: Lemma Qquadratic_sign_pres_fraction : 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), Qmult (Qplus (Qplus (Qplus (Qmult (Qmult (qnew_a a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (Qpos (qnew_p1 a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero))) (Qpos (qnew_p2 a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero))) (Qmult (qnew_b a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (Qpos (qnew_p1 a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero)))) (Qmult (qnew_c a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (Qpos (qnew_p2 a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero)))) (qnew_d a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero)) (Qinv (Qplus (Qplus (Qplus (Qmult (Qmult (qnew_e a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (Qpos (qnew_p1 a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero))) (Qpos (qnew_p2 a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero))) (Qmult (qnew_f a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (Qpos (qnew_p1 a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero)))) (Qmult (qnew_g a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (Qpos (qnew_p2 a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero)))) (qnew_h a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero))) = Qmult (Qplus (Qplus (Qplus (Qmult (Qmult a (Qpos p1)) (Qpos p2)) (Qmult b (Qpos p1))) (Qmult c (Qpos p2))) d) (Qinv (Qplus (Qplus (Qplus (Qmult (Qmult e (Qpos p1)) (Qpos p2)) (Qmult f (Qpos p1))) (Qmult g (Qpos p2))) h)).
proof: Proof. fix Qquadratic_sign_pres_fraction 9. intros a b c d e f g h. unfold qnew_a, qnew_b, qnew_c, qnew_d, qnew_e, qnew_f, qnew_g, qnew_h, qnew_p1, qnew_p2 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 Qquadratic_sign_pres_fraction; 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)). case (Z_lt_dec 2 o2). clear Qquadratic_sign_pres_fraction; 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)). case (Z_lt_dec o2 (-2)). clear Qquadratic_sign_pres_fraction; 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)). 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_unfolded; rewrite <- Qquadratic_sign_pres_fraction with (H_Qquadratic_sg_denom_nonzero := 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 Qquadratic_sign_pres_fraction; 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)). case (Z_lt_dec o1 (-2)). clear Qquadratic_sign_pres_fraction; 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)). 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_unfolded; rewrite <- Qquadratic_sign_pres_fraction with (H_Qquadratic_sg_denom_nonzero := 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 Qquadratic_sign_pres_fraction; 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))). intro H_inside_1'. case (inside_square_2_dec_inf o1 o2). clear Qquadratic_sign_pres_fraction; 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))). 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_unfolded; rewrite <- Qquadratic_sign_pres_fraction with (H_Qquadratic_sg_denom_nonzero := 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 Qquadratic_sign_pres_fraction; 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)). case (Z_lt_dec 2 o2). clear Qquadratic_sign_pres_fraction; 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)). case (Z_lt_dec o2 (-2)). clear Qquadratic_sign_pres_fraction; 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)). 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_unfolded; rewrite <- Qquadratic_sign_pres_fraction with (H_Qquadratic_sg_denom_nonzero := 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 Qquadratic_sign_pres_fraction; 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)). case (Z_lt_dec o1 (-2)). clear Qquadratic_sign_pres_fraction; 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)). 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_unfolded; rewrite <- Qquadratic_sign_pres_fraction with (H_Qquadratic_sg_denom_nonzero := 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 Qquadratic_sign_pres_fraction; 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))). intro H_inside_1'. case (inside_square_2_dec_inf o1 o2). clear Qquadratic_sign_pres_fraction; 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))). 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_unfolded; rewrite <- Qquadratic_sign_pres_fraction with (H_Qquadratic_sg_denom_nonzero := Qquadratic_signok_2 e f g h xs ys H_Qquadratic_sg_denom_nonzero); reflexivity. clear o1 o2 Qquadratic_sign_pres_fraction. 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_unfolded. unfold snd in |- *. unfold fst in |- *. repeat rewrite Zplus_0_l. repeat rewrite Qmult_one_right. replace na with (new_a (a + b) (c + d) (e + f) (g + h) (nR xs) H_Qhomographic_sg_denom_nonzero); trivial. replace nb with (new_b (a + b) (c + d) (e + f) (g + h) (nR xs) H_Qhomographic_sg_denom_nonzero); trivial. replace nc with (new_c (a + b) (c + d) (e + f) (g + h) (nR xs) H_Qhomographic_sg_denom_nonzero); trivial. replace nd with (new_d (a + b) (c + d) (e + f) (g + h) (nR xs) H_Qhomographic_sg_denom_nonzero); trivial. replace l3 with (new_p (a + b) (c + d) (e + f) (g + h) (nR xs) H_Qhomographic_sg_denom_nonzero); trivial. rewrite sg_pres_fraction. repeat rewrite Z_to_Qplus. clear L3 l1 l2 l3 na nb nc nd; apply f_equal2 with Q Q; try apply f_equal with Q; abstract ring. 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 Qquadratic_sign_pres_fraction; 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)). case (Z_lt_dec 2 o2). clear Qquadratic_sign_pres_fraction; 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)). case (Z_lt_dec o2 (-2)). clear Qquadratic_sign_pres_fraction; 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)). 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_unfolded; rewrite <- Qquadratic_sign_pres_fraction with (H_Qquadratic_sg_denom_nonzero := 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 Qquadratic_sign_pres_fraction; 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)). case (Z_lt_dec o1 (-2)). clear Qquadratic_sign_pres_fraction; 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)). 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_unfolded; rewrite <- Qquadratic_sign_pres_fraction with (H_Qquadratic_sg_denom_nonzero := 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 Qquadratic_sign_pres_fraction; 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))). intro H_inside_1'. case (inside_square_2_dec_inf o1 o2). clear Qquadratic_sign_pres_fraction; 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))). 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_unfolded; rewrite <- Qquadratic_sign_pres_fraction with (H_Qquadratic_sg_denom_nonzero := 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 Qquadratic_sign_pres_fraction; 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)). case (Z_lt_dec 2 o2). clear Qquadratic_sign_pres_fraction; 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)). case (Z_lt_dec o2 (-2)). clear Qquadratic_sign_pres_fraction; 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)). 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_unfolded; rewrite <- Qquadratic_sign_pres_fraction with (H_Qquadratic_sg_denom_nonzero := 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 Qquadratic_sign_pres_fraction; 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)). case (Z_lt_dec o1 (-2)). clear Qquadratic_sign_pres_fraction; 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)). 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_unfolded; rewrite <- Qquadratic_sign_pres_fraction with (H_Qquadratic_sg_denom_nonzero := 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 Qquadratic_sign_pres_fraction; 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))). intro H_inside_1'. case (inside_square_2_dec_inf o1 o2). clear Qquadratic_sign_pres_fraction; 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))). 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_unfolded; rewrite <- Qquadratic_sign_pres_fraction with (H_Qquadratic_sg_denom_nonzero := Qquadratic_signok_4 e f g h xs ys H_Qquadratic_sg_denom_nonzero); reflexivity. clear o1 o2 Qquadratic_sign_pres_fraction. 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_unfolded. unfold snd in |- *. unfold fst in |- *. repeat rewrite Zplus_0_l. repeat rewrite Qmult_one_right. replace na with (new_a (a + b) (c + d) (e + f) (g + h) (dL xs) H_Qhomographic_sg_denom_nonzero); trivial. replace nb with (new_b (a + b) (c + d) (e + f) (g + h) (dL xs) H_Qhomographic_sg_denom_nonzero); trivial. replace nc with (new_c (a + b) (c + d) (e + f) (g + h) (dL xs) H_Qhomographic_sg_denom_nonzero); trivial. replace nd with (new_d (a + b) (c + d) (e + f) (g + h) (dL xs) H_Qhomographic_sg_denom_nonzero); trivial. replace l3 with (new_p (a + b) (c + d) (e + f) (g + h) (dL xs) H_Qhomographic_sg_denom_nonzero); trivial. rewrite sg_pres_fraction. repeat rewrite Z_to_Qplus. clear L3 l1 l2 l3 na nb nc nd; apply f_equal2 with Q Q; try apply f_equal with Q; abstract ring. clear o1 o2 Qquadratic_sign_pres_fraction. intros p2 H_Qquadratic_sg_denom_nonzero. 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_unfolded. unfold snd in |- *. unfold fst in |- *. repeat rewrite Zplus_0_l. repeat rewrite Qmult_one_right. replace na with (new_a (a + c) (b + d) (e + g) (f + h) p2 H_Qhomographic_sg_denom_nonzero); trivial. replace nb with (new_b (a + c) (b + d) (e + g) (f + h) p2 H_Qhomographic_sg_denom_nonzero); trivial. replace nc with (new_c (a + c) (b + d) (e + g) (f + h) p2 H_Qhomographic_sg_denom_nonzero); trivial. replace nd with (new_d (a + c) (b + d) (e + g) (f + h) p2 H_Qhomographic_sg_denom_nonzero); trivial. replace l3 with (new_p (a + c) (b + d) (e + g) (f + h) p2 H_Qhomographic_sg_denom_nonzero); trivial. rewrite sg_pres_fraction. repeat rewrite Z_to_Qplus. clear L3 l1 l2 l3 na nb nc nd; apply f_equal2 with Q Q; try apply f_equal with Q; abstract ring. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)