proposition: Lemma Qhomographic_Qpositive_to_Q_homographicAcc_neg_1 : forall (a b c d : Z) (p : Qpositive) (H_hsign : Qhomographic_sg_denom_nonzero c d p), (a * d)%Z <> (b * c)%Z -> h_sign a b c d p H_hsign = (-1)%Z -> (Z.sgn (new_a a b c d p H_hsign + new_b a b c d p H_hsign) < 0)%Z -> homographicAcc (- new_a a b c d p H_hsign) (- new_b a b c d p H_hsign) (new_c a b c d p H_hsign) (new_d a b c d p H_hsign) (new_p a b c d p H_hsign).
proof: Proof. intros a b c d p H_hsign ad_neq_bc l1_eq__minus_one z. set (na := new_a a b c d p H_hsign) in *. set (nb := new_b a b c d p H_hsign) in *. set (nc := new_c a b c d p H_hsign) in *. set (nd := new_d a b c d p H_hsign) in *. set (l3 := new_p a b c d p H_hsign) in *. assert (H : Qhomographic_sign a b c d p H_hsign = ((-1)%Z, (na, (nb, (nc, nd)), l3))). unfold na, nb, nc, nd, l3 in |- *. rewrite <- l1_eq__minus_one. unfold new_a, new_b, new_c, new_d, new_p in |- *. replace (h_sign a b c d p H_hsign) with (fst (Qhomographic_sign a b c d p H_hsign)); [ idtac | reflexivity ]; repeat rewrite <- pair_1; reflexivity. destruct l3 as [p0| p0| ]. apply homographicAcc_wf. rewrite <- Zopp_plus_distr. apply Zlt_neg_opp. apply Zsgn_11. assumption. generalize (sg_neg_1 a b c d p H_hsign na nb nc nd (nR p0) H). intros. case H0. intro. elim a0. intros. apply False_ind. generalize (Zsgn_11 (na + nb) z). intro. apply Z.lt_irrefl with 0%Z. apply Z.lt_trans with (na + nb)%Z. assumption. assumption. intros. elim a0. intros. assumption. generalize (sg_neg_2 a b c d p H_hsign na nb nc nd (nR p0) H). intro. case H0. intro. case s. intro. apply False_ind. elim a0. intros. elim H2. intros. apply Z.lt_irrefl with 0%Z. apply Z.le_lt_trans with (na + nb)%Z. rewrite Zplus_0_r_reverse with 0%Z. apply Zplus_le_compat. assumption. assumption. apply Zsgn_11. assumption. intro. elim a0. intros. apply Zle_neg_opp. assumption. intro. discriminate e. generalize (sg_neg_2 a b c d p H_hsign na nb nc nd (nR p0) H). intro. case H0. intro. case s. intro. elim a0. intros. elim H2. intros. apply False_ind. apply Z.lt_irrefl with 0%Z. apply Z.le_lt_trans with (na + nb)%Z. rewrite Zplus_0_r_reverse with 0%Z. apply Zplus_le_compat. assumption. assumption. apply Zsgn_11. assumption. intros. elim a0. intros. elim H2. intros. apply Zle_neg_opp. assumption. intro. discriminate e. generalize (sg_neg_2 a b c d p H_hsign na nb nc nd (nR p0) H). intro. case H0. intro. case s. intro. elim a0. intros. elim H2. intros. apply False_ind. apply Z.lt_irrefl with 0%Z. apply Z.le_lt_trans with (na + nb)%Z. rewrite Zplus_0_r_reverse with 0%Z. apply Zplus_le_compat. assumption. assumption. apply Zsgn_11. assumption. intros. elim a0. intros. elim H2. intros. elim H4. intros. assumption. intro. discriminate e. generalize (sg_neg_2 a b c d p H_hsign na nb nc nd (nR p0) H). intro. case H0. intro. case s. intro. elim a0. intros. elim H2. intros. apply False_ind. apply Z.lt_irrefl with 0%Z. apply Z.le_lt_trans with (na + nb)%Z. rewrite Zplus_0_r_reverse with 0%Z. apply Zplus_le_compat. assumption. assumption. apply Zsgn_11. assumption. intro. elim a0. intros. elim H2. intros. elim H4. intros. assumption. intro. discriminate e. apply homographicAcc_wf. rewrite <- Zopp_plus_distr. apply Zlt_neg_opp. apply Zsgn_11. assumption. generalize (sg_neg_1 a b c d p H_hsign na nb nc nd (dL p0) H). intros. case H0. intro. elim a0. intros. apply False_ind. generalize (Zsgn_11 (na + nb) z). intro. apply Z.lt_irrefl with 0%Z. apply Z.lt_trans with (na + nb)%Z. assumption. assumption. intros. elim a0. intros. assumption. generalize (sg_neg_2 a b c d p H_hsign na nb nc nd (dL p0) H). intro. case H0. intro. case s. intro. apply False_ind. elim a0. intros. elim H2. intros. apply Z.lt_irrefl with 0%Z. apply Z.le_lt_trans with (na + nb)%Z. rewrite Zplus_0_r_reverse with 0%Z. apply Zplus_le_compat. assumption. assumption. apply Zsgn_11. assumption. intro. elim a0. intros. apply Zle_neg_opp. assumption. intro. discriminate e. generalize (sg_neg_2 a b c d p H_hsign na nb nc nd (dL p0) H). intro. case H0. intro. case s. intro. elim a0. intros. elim H2. intros. apply False_ind. apply Z.lt_irrefl with 0%Z. apply Z.le_lt_trans with (na + nb)%Z. rewrite Zplus_0_r_reverse with 0%Z. apply Zplus_le_compat. assumption. assumption. apply Zsgn_11. assumption. intros. elim a0. intros. elim H2. intros. apply Zle_neg_opp. assumption. intro. discriminate e. generalize (sg_neg_2 a b c d p H_hsign na nb nc nd (dL p0) H). intro. case H0. intro. case s. intro. elim a0. intros. elim H2. intros. apply False_ind. apply Z.lt_irrefl with 0%Z. apply Z.le_lt_trans with (na + nb)%Z. rewrite Zplus_0_r_reverse with 0%Z. apply Zplus_le_compat. assumption. assumption. apply Zsgn_11. assumption. intros. elim a0. intros. elim H2. intros. elim H4. intros. assumption. intro. discriminate e. generalize (sg_neg_2 a b c d p H_hsign na nb nc nd (dL p0) H). intro. case H0. intro. case s. intro. elim a0. intros. elim H2. intros. apply False_ind. apply Z.lt_irrefl with 0%Z. apply Z.le_lt_trans with (na + nb)%Z. rewrite Zplus_0_r_reverse with 0%Z. apply Zplus_le_compat. assumption. assumption. apply Zsgn_11. assumption. intro. elim a0. intros. elim H2. intros. elim H4. intros. assumption. intro. discriminate e. apply homographicacc0. reflexivity. rewrite <- Zopp_plus_distr. apply Zlt_neg_opp. apply Zsgn_11. assumption. generalize (sg_neg_1 a b c d p H_hsign na nb nc nd One H). intros. case H0. intro. elim a0. intros. apply False_ind. generalize (Zsgn_11 (na + nb) z). intro. apply Z.lt_irrefl with 0%Z. apply Z.lt_trans with (na + nb)%Z. assumption. assumption. intro. elim a0. intros. assumption. Defined.