proposition: Lemma Qquadratic_Qpositive_to_Q_equal : forall (a b c d e f g h : Z) (p1 p2 : Qpositive) (H_Qquadratic_sg_denom_nonzero1 H_Qquadratic_sg_denom_nonzero2 : Qquadratic_sg_denom_nonzero e f g h p1 p2), Qquadratic_Qpositive_to_Q a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero1 = Qquadratic_Qpositive_to_Q a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero2.
proof: Proof. intros a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero1. functional induction (Qquadratic_Qpositive_to_Q a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero1); intros; Clear_eq_. rewrite (Qquadratic_Qpositive_to_Q_3 _ _ _ _ _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 n s); reflexivity. rewrite (Qquadratic_Qpositive_to_Q_2 _ _ _ _ _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 n s); reflexivity. rewrite (Qquadratic_Qpositive_to_Q_1 _ _ _ _ _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 n s); reflexivity. rewrite (Qquadratic_Qpositive_to_Q_0 _ _ _ _ _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 n s); reflexivity. rewrite (q_sign_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero1 H_Qquadratic_sg_denom_nonzero2) in e2; rewrite (Qquadratic_Qpositive_to_Q_4 _ _ _ _ _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 n e2) ; reflexivity. Absurd_q_sign_. assert (H : Z.sgn (qnew_a a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero2 + qnew_b a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero2 + qnew_c a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero2 + qnew_d a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero2) = 1%Z). rewrite (qnew_a_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1); rewrite (qnew_b_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1); rewrite (qnew_c_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1); rewrite (qnew_d_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1); assumption. rewrite (Qquadratic_Qpositive_to_Q_5 _ _ _ _ _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 n (trans_eq (q_sign_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1) e2) H (Qquadratic_Qpositive_to_Q_quadraticAcc_pos_1 _ _ _ _ _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 n (trans_eq (q_sign_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1) e2) H)) ; apply f_equal with Qpositive; apply Qquadratic_Qpositive_to_Qpositive_equal_strong; [ apply qnew_a_equal | apply qnew_b_equal | apply qnew_c_equal | apply qnew_d_equal | apply qnew_e_equal | apply qnew_f_equal | apply qnew_g_equal | apply qnew_h_equal | apply qnew_p1_equal | apply qnew_p2_equal ]. assert (H : Z.sgn (qnew_a a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero2 + qnew_b a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero2 + qnew_c a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero2 + qnew_d a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero2) = (-1)%Z). rewrite (qnew_a_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1); rewrite (qnew_b_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1); rewrite (qnew_c_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1); rewrite (qnew_d_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1); assumption. rewrite (Qquadratic_Qpositive_to_Q_6 _ _ _ _ _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 n (trans_eq (q_sign_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1) e2) H (Qquadratic_Qpositive_to_Q_quadraticAcc_pos_2 _ _ _ _ _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 n (trans_eq (q_sign_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1) e2) H)) . apply f_equal with Qpositive; apply Qquadratic_Qpositive_to_Qpositive_equal_strong; try apply f_equal with Z; [ apply qnew_a_equal | apply qnew_b_equal | apply qnew_c_equal | apply qnew_d_equal | apply qnew_e_equal | apply qnew_f_equal | apply qnew_g_equal | apply qnew_h_equal | apply qnew_p1_equal | apply qnew_p2_equal ]. Absurd_q_sign_. assert (H : Z.sgn (qnew_a a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero2 + qnew_b a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero2 + qnew_c a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero2 + qnew_d a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero2) = 1%Z). rewrite (qnew_a_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1); rewrite (qnew_b_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1); rewrite (qnew_c_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1); rewrite (qnew_d_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1); assumption. rewrite (Qquadratic_Qpositive_to_Q_7 _ _ _ _ _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 n (trans_eq (q_sign_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1) e1) H (Qquadratic_Qpositive_to_Q_quadraticAcc_neg_1 _ _ _ _ _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 n (trans_eq (q_sign_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1) e1) H)) . apply f_equal with Qpositive; apply Qquadratic_Qpositive_to_Qpositive_equal_strong; try apply f_equal with Z; [ apply qnew_a_equal | apply qnew_b_equal | apply qnew_c_equal | apply qnew_d_equal | apply qnew_e_equal | apply qnew_f_equal | apply qnew_g_equal | apply qnew_h_equal | apply qnew_p1_equal | apply qnew_p2_equal ]. assert (H : Z.sgn (qnew_a a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero2 + qnew_b a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero2 + qnew_c a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero2 + qnew_d a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero2) = (-1)%Z). rewrite (qnew_a_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1); rewrite (qnew_b_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1); rewrite (qnew_c_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1); rewrite (qnew_d_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1); assumption. rewrite (Qquadratic_Qpositive_to_Q_8 _ _ _ _ _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 n (trans_eq (q_sign_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1) e1) H (Qquadratic_Qpositive_to_Q_quadraticAcc_neg_2 _ _ _ _ _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 n (trans_eq (q_sign_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 H_Qquadratic_sg_denom_nonzero1) e1) H)) . apply f_equal with Qpositive; apply Qquadratic_Qpositive_to_Qpositive_equal_strong; try apply f_equal with Z; [ apply qnew_a_equal | apply qnew_b_equal | apply qnew_c_equal | apply qnew_d_equal | apply qnew_e_equal | apply qnew_f_equal | apply qnew_g_equal | apply qnew_h_equal | apply qnew_p1_equal | apply qnew_p2_equal ]. Qed.
imports: Coq(FunInd) QArithSternBrocot(homographic_correctness)