proposition: Lemma Qquadratic_Qpositive_to_Q_quadraticAcc_pos_2 : 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), ~ same_ratio a b c d e f g h -> q_sign a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero = 1%Z -> Z.sgn (qnew_a a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero + qnew_b a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero + qnew_c 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) = (-1)%Z -> quadraticAcc (- qnew_a a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (- qnew_b a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (- qnew_c 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) (- qnew_e a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (- qnew_f a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (- qnew_g 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) (qnew_p1 a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (qnew_p2 a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero).
proof: Proof. intros a b c d e f g h p1 p2 H_qsign not_same_ratio_abcdefgh l1_eq_one na_nb_nc_nd_eq_minus_one. set (na := qnew_a a b c d e f g h p1 p2 H_qsign) in *. set (nb := qnew_b a b c d e f g h p1 p2 H_qsign) in *. set (nc := qnew_c a b c d e f g h p1 p2 H_qsign) in *. set (nd := qnew_d a b c d e f g h p1 p2 H_qsign) in *. set (ne := qnew_e a b c d e f g h p1 p2 H_qsign) in *. set (nf := qnew_f a b c d e f g h p1 p2 H_qsign) in *. set (ng := qnew_g a b c d e f g h p1 p2 H_qsign) in *. set (nh := qnew_h a b c d e f g h p1 p2 H_qsign) in *. set (np1 := qnew_p1 a b c d e f g h p1 p2 H_qsign) in *. set (np2 := qnew_p2 a b c d e f g h p1 p2 H_qsign) in *. assert (H : Qquadratic_sign a b c d e f g h p1 p2 H_qsign = (1%Z, (na, (nb, (nc, nd)), (ne, (nf, (ng, nh))), (np1, np2)))). unfold na, nb, nc, nd, ne, nf, ng, nh, np1, np2 in |- *. rewrite <- l1_eq_one. unfold qnew_a, qnew_b, qnew_c, qnew_d, qnew_e, qnew_f, qnew_g, qnew_h, qnew_p1, qnew_p2 in |- *. replace (q_sign a b c d e f g h p1 p2 H_qsign) with (fst (Qquadratic_sign a b c d e f g h p1 p2 H_qsign)); [ idtac | reflexivity ]; repeat rewrite <- pair_1; reflexivity. generalize (Qquadratic_sign_pos_1 a b c d e f g h p1 p2 H_qsign na nb nc nd ne nf ng nh np1 np2 H). intros [(H1, _)| (H_nabcd, H_nefgh)]; [ apply False_ind; generalize (Zsgn_10 _ na_nb_nc_nd_eq_minus_one); apply Zlt_asym; assumption | idtac ]. destruct np1 as [p| p| ]. destruct np2 as [p0| p0| ]. apply quadraticAcc_wf; solve [ lia | generalize (Qquadratic_sign_pos_2 a b c d e f g h p1 p2 H_qsign na nb nc nd ne nf ng nh (nR p) (nR p0) H); intros [[[[[[(Ha, (Hb, (Hc, (Hd, (He, (Hf, (Hg, Hh)))))))| (Ha, (Hb, (Hc, (Hd, (He, (Hf, (Hg, Hh)))))))]| (H_discriminate_me, _)]| (H_discriminate_me, _)]| (H_discriminate_me, _)]| (_, (H_discriminate_me,_))]| (_, (H_discriminate_me,_))]; [ apply False_ind; generalize H_nabcd; apply Zle_not_lt; repeat apply Zplus_le_0_compat; assumption | apply Zle_neg_opp; assumption | discriminate H_discriminate_me | discriminate H_discriminate_me | discriminate H_discriminate_me | discriminate H_discriminate_me | discriminate H_discriminate_me ] ]. apply quadraticAcc_wf; solve [ lia | generalize (Qquadratic_sign_pos_2 a b c d e f g h p1 p2 H_qsign na nb nc nd ne nf ng nh (nR p) (dL p0) H); intros [[[[[[(Ha, (Hb, (Hc, (Hd, (He, (Hf, (Hg, Hh)))))))| (Ha, (Hb, (Hc, (Hd, (He, (Hf, (Hg, Hh)))))))]| (H_discriminate_me, _)]| (H_discriminate_me, _)]| (H_discriminate_me, _)]| (_, (H_discriminate_me,_))]| (_, (H_discriminate_me,_))]; [ apply False_ind; generalize H_nabcd; apply Zle_not_lt; repeat apply Zplus_le_0_compat; assumption | apply Zle_neg_opp; assumption | discriminate H_discriminate_me | discriminate H_discriminate_me | discriminate H_discriminate_me | discriminate H_discriminate_me | discriminate H_discriminate_me ] ]. apply quadraticacc0'. discriminate. reflexivity. apply homographicAcc_wf; solve [ lia | generalize (Qquadratic_sign_pos_2 a b c d e f g h p1 p2 H_qsign na nb nc nd ne nf ng nh (nR p) One H); intros [[[[[[(Ha, (Hb, (Hc, (Hd, (He, (Hf, (Hg, Hh)))))))| (Ha, (Hb, (Hc, (Hd, (He, (Hf, (Hg, Hh)))))))]| (H_discriminate_me, _)]| (H_discriminate_me, _)]| (H_discriminate_me, _)]| (_, (_, (Hab, (Hcd, (Hef, Hgh)))))]| (_, (_, (Hab, (Hcd, (Hef, Hgh)))))]; [ apply False_ind; generalize H_nabcd; apply Zle_not_lt; repeat apply Zplus_le_0_compat; assumption | lia | discriminate H_discriminate_me | discriminate H_discriminate_me | discriminate H_discriminate_me | apply False_ind; generalize H_nabcd; apply Zle_not_lt; rewrite <- Zplus_assoc; apply Zplus_le_0_compat; assumption | lia ] ]. destruct np2 as [p0| p0| ]. apply quadraticAcc_wf; solve [ lia | generalize (Qquadratic_sign_pos_2 a b c d e f g h p1 p2 H_qsign na nb nc nd ne nf ng nh (dL p) (nR p0) H); intros [[[[[[(Ha, (Hb, (Hc, (Hd, (He, (Hf, (Hg, Hh)))))))| (Ha, (Hb, (Hc, (Hd, (He, (Hf, (Hg, Hh)))))))]| (H_discriminate_me, _)]| (H_discriminate_me, _)]| (H_discriminate_me, _)]| (_, (H_discriminate_me,_))]| (_, (H_discriminate_me,_))]; [ apply False_ind; generalize H_nabcd; apply Zle_not_lt; repeat apply Zplus_le_0_compat; assumption | apply Zle_neg_opp; assumption | discriminate H_discriminate_me | discriminate H_discriminate_me | discriminate H_discriminate_me | discriminate H_discriminate_me | discriminate H_discriminate_me ] ]. apply quadraticAcc_wf; solve [ lia | generalize (Qquadratic_sign_pos_2 a b c d e f g h p1 p2 H_qsign na nb nc nd ne nf ng nh (dL p) (dL p0) H); intros [[[[[[(Ha, (Hb, (Hc, (Hd, (He, (Hf, (Hg, Hh)))))))| (Ha, (Hb, (Hc, (Hd, (He, (Hf, (Hg, Hh)))))))]| (H_discriminate_me, _)]| (H_discriminate_me, _)]| (H_discriminate_me, _)]| (_, (H_discriminate_me,_))]| (_, (H_discriminate_me,_))]; [ apply False_ind; generalize H_nabcd; apply Zle_not_lt; repeat apply Zplus_le_0_compat; assumption | apply Zle_neg_opp; assumption | discriminate H_discriminate_me | discriminate H_discriminate_me | discriminate H_discriminate_me | discriminate H_discriminate_me | discriminate H_discriminate_me ] ]. apply quadraticacc0'. discriminate. reflexivity. apply homographicAcc_wf; solve [ lia | generalize (Qquadratic_sign_pos_2 a b c d e f g h p1 p2 H_qsign na nb nc nd ne nf ng nh (dL p) One H); intros [[[[[[(Ha, (Hb, (Hc, (Hd, (He, (Hf, (Hg, Hh)))))))| (Ha, (Hb, (Hc, (Hd, (He, (Hf, (Hg, Hh)))))))]| (H_discriminate_me, _)]| (H_discriminate_me, _)]| (H_discriminate_me, _)]| (_, (_, (Hab, (Hcd, (Hef, Hgh)))))]| (_, (_, (Hab, (Hcd, (Hef, Hgh)))))]; [ apply False_ind; generalize H_nabcd; apply Zle_not_lt; repeat apply Zplus_le_0_compat; assumption | lia | discriminate H_discriminate_me | discriminate H_discriminate_me | discriminate H_discriminate_me | apply False_ind; generalize H_nabcd; apply Zle_not_lt; rewrite <- Zplus_assoc; apply Zplus_le_0_compat; assumption | lia ] ]. apply quadraticacc0. reflexivity. destruct np2 as [p| p| ]. apply homographicAcc_wf; solve [ lia | generalize (Qquadratic_sign_pos_2 a b c d e f g h p1 p2 H_qsign na nb nc nd ne nf ng nh One (nR p) H); intros [[[[[[(Ha, (Hb, (Hc, (Hd, (He, (Hf, (Hg, Hh)))))))| (Ha, (Hb, (Hc, (Hd, (He, (Hf, (Hg, Hh)))))))]| (_, (Hab, (Hcd, (Hef, Hgh))))]| (_, (Hab, (Hcd, (Hef, Hgh))))]| (_, H_discriminate_me)]| (_, (H_discriminate_me,_))]| (_, (H_discriminate_me,_))]; [ apply False_ind; generalize H_nabcd; apply Zle_not_lt; repeat apply Zplus_le_0_compat; assumption | apply Zplus_le_0_compat; apply Zle_neg_opp; assumption | apply False_ind; generalize H_nabcd; apply Zle_not_lt; lia | rewrite <- Zopp_plus_distr; apply Zle_neg_opp; assumption | discriminate H_discriminate_me | discriminate H_discriminate_me | discriminate H_discriminate_me ] ]. apply homographicAcc_wf; solve [ lia | generalize (Qquadratic_sign_pos_2 a b c d e f g h p1 p2 H_qsign na nb nc nd ne nf ng nh One (dL p) H); intros [[[[[[(Ha, (Hb, (Hc, (Hd, (He, (Hf, (Hg, Hh)))))))| (Ha, (Hb, (Hc, (Hd, (He, (Hf, (Hg, Hh)))))))]| (_, (Hab, (Hcd, (Hef, Hgh))))]| (_, (Hab, (Hcd, (Hef, Hgh))))]| (_, H_discriminate_me)]| (_, (H_discriminate_me,_))]| (_, (H_discriminate_me,_))]; [ apply False_ind; generalize H_nabcd; apply Zle_not_lt; repeat apply Zplus_le_0_compat; assumption | apply Zplus_le_0_compat; apply Zle_neg_opp; assumption | apply False_ind; generalize H_nabcd; apply Zle_not_lt; lia | rewrite <- Zopp_plus_distr; apply Zle_neg_opp; assumption | discriminate H_discriminate_me | discriminate H_discriminate_me | discriminate H_discriminate_me ] ]. apply homographicacc0; reflexivity || lia. Qed.