proposition: Lemma sg_neg_1 : forall (a b c d : Z) (p : Qpositive) (H_Qhomographic_sg_denom_nonzero : Qhomographic_sg_denom_nonzero c d p) (na nb nc nd : Z) (np : Qpositive), Qhomographic_sign a b c d p H_Qhomographic_sg_denom_nonzero = ((-1)%Z, (na, (nb, (nc, nd)), np)) -> {(0 < na + nb)%Z /\ (nc + nd < 0)%Z} + {(na + nb < 0)%Z /\ (0 < nc + nd)%Z}.
proof: Proof. fix sg_neg_1 5. intros a b c d p H_Qhomographic_sg_denom_nonzero na nb nc nd np H_sg. set (o1 := outside_interval a b) in *. set (o2 := outside_interval c d) in *. destruct p as [p| p| ]. case (Z_zerop b); intro Hb. case (Z_zerop d); intro Hd. generalize (Qhomographic_sign_nR_1 a b c d (nR p) p H_Qhomographic_sg_denom_nonzero (refl_equal (nR p)) Hb Hd); intro; assert (H6 : ((-1)%Z, (na, (nb, (nc, nd)), np)) = ((Z.sgn a * Z.sgn c)%Z, (a, (b, (c, d)), nR p))); [ apply trans_eq with (Qhomographic_sign a b c d (nR p) H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption | elim (sg_tuple_equal (-1) na nb nc nd np (Z.sgn a * Z.sgn c) a b c d (nR p) H6); intros H_ac ((H8, (H9, (H10, H11))), H12); repeat match goal with | id1:(?X1 = ?X2) |- ?X3 => rewrite id1 end; repeat rewrite Zplus_0_r; apply Zsgn_17; rewrite Zsgn_15; symmetry in |- *; assumption ]. case (Z_lt_dec 0 o2); intros Ho2. generalize (Qhomographic_sign_nR_2 a b c d (nR p) p H_Qhomographic_sg_denom_nonzero (refl_equal (nR p)) Hb Hd Ho2); intro; assert (H6 : ((-1)%Z, (na, (nb, (nc, nd)), np)) = (Z.sgn a, (a, (b, (c, d)), nR p))); [ apply trans_eq with (Qhomographic_sign a b c d (nR p) H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption | elim (sg_tuple_equal (-1) na nb nc nd np (Z.sgn a) a b c d (nR p) H6); intros H_a ((H8, (H9, (H10, H11))), H12); repeat match goal with | id1:(?X1 = ?X2) |- ?X3 => rewrite id1 end; repeat rewrite Zplus_0_r; right; split; [ apply Zsgn_10; symmetry in |- * | apply Zsgn_19 ]; assumption ]. case (Z_lt_dec o2 0); intros Ho2'. generalize (Qhomographic_sign_nR_3 a b c d (nR p) p H_Qhomographic_sg_denom_nonzero (refl_equal (nR p)) Hb Hd Ho2 Ho2'); intro; assert (H6 : ((-1)%Z, (na, (nb, (nc, nd)), np)) = ((- Z.sgn a)%Z, (a, (b, (c, d)), nR p))); [ apply trans_eq with (Qhomographic_sign a b c d (nR p) H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption | elim (sg_tuple_equal (-1) na nb nc nd np (- Z.sgn a) a b c d (nR p) H6); intros H_a ((H8, (H9, (H10, H11))), H12); repeat match goal with | id1:(?X1 = ?X2) |- ?X3 => rewrite id1 end; repeat rewrite Zplus_0_r; left; split; [ apply Zsgn_9; symmetry in |- *; apply Z.opp_inj | apply Zsgn_20 ]; assumption ]. generalize (Qhomographic_sign_nR_4 a b c d (nR p) p (Qhomographic_signok_2 c d p H_Qhomographic_sg_denom_nonzero) H_Qhomographic_sg_denom_nonzero Hb Hd Ho2 Ho2'); intro; apply (sg_neg_1 a (a + b)%Z c (c + d)%Z p (Qhomographic_signok_2 c d p H_Qhomographic_sg_denom_nonzero) na nb nc nd np); apply trans_eq with (Qhomographic_sign a b c d (nR p) H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption. case (Z_zerop d); intro Hd. case (Z_lt_dec 0 o1); intro Ho1. generalize (Qhomographic_sign_nR_5 a b c d (nR p) p H_Qhomographic_sg_denom_nonzero (refl_equal (nR p)) Hb Hd Ho1); intro; assert (H6 : ((-1)%Z, (na, (nb, (nc, nd)), np)) = (Z.sgn c, (a, (b, (c, d)), nR p))); [ apply trans_eq with (Qhomographic_sign a b c d (nR p) H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption | elim (sg_tuple_equal (-1) na nb nc nd np (Z.sgn c) a b c d (nR p) H6); intros H_a ((H8, (H9, (H10, H11))), H12); repeat match goal with | id1:(?X1 = ?X2) |- ?X3 => rewrite id1 end; repeat rewrite Zplus_0_r; left; split; [ apply Zsgn_19 | apply Zsgn_10; symmetry in |- * ]; assumption ]. case (Z_lt_dec o1 0); intros Ho1'. generalize (Qhomographic_sign_nR_6 a b c d (nR p) p H_Qhomographic_sg_denom_nonzero (refl_equal (nR p)) Hb Hd Ho1 Ho1'); intro; assert (H6 : ((-1)%Z, (na, (nb, (nc, nd)), np)) = ((- Z.sgn c)%Z, (a, (b, (c, d)), nR p))); [ apply trans_eq with (Qhomographic_sign a b c d (nR p) H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption | elim (sg_tuple_equal (-1) na nb nc nd np (- Z.sgn c) a b c d (nR p) H6); intros H_a ((H8, (H9, (H10, H11))), H12); repeat match goal with | id1:(?X1 = ?X2) |- ?X3 => rewrite id1 end; repeat rewrite Zplus_0_r; right; split; [ apply Zsgn_20 | apply Zsgn_9; symmetry in |- *; apply Z.opp_inj ]; assumption ]. generalize (Qhomographic_sign_nR_7 a b c d (nR p) p (Qhomographic_signok_2 c d p H_Qhomographic_sg_denom_nonzero) H_Qhomographic_sg_denom_nonzero Hb Hd Ho1 Ho1'); intro; apply (sg_neg_1 a (a + b)%Z c (c + d)%Z p (Qhomographic_signok_2 c d p H_Qhomographic_sg_denom_nonzero) na nb nc nd np); apply trans_eq with (Qhomographic_sign a b c d (nR p) H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption. case (inside_interval_1_dec_inf o1 o2); intro H_inside_1. generalize (Qhomographic_sign_nR_8 a b c d (nR p) p H_Qhomographic_sg_denom_nonzero (refl_equal (nR p)) Hb Hd H_inside_1); intro; assert (H6 : ((-1)%Z, (na, (nb, (nc, nd)), np)) = (1%Z, (a, (b, (c, d)), nR p))); [ apply trans_eq with (Qhomographic_sign a b c d (nR p) H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption | elim (sg_tuple_equal (-1) na nb nc nd np 1 a b c d (nR p) H6); intros hl H_rest; discriminate hl ]. case (inside_interval_2_dec_inf o1 o2); intro H_inside_2. generalize (Qhomographic_sign_nR_9 a b c d (nR p) p H_Qhomographic_sg_denom_nonzero (refl_equal (nR p)) Hb Hd H_inside_1 H_inside_2); intro; assert (H6 : ((-1)%Z, (na, (nb, (nc, nd)), np)) = ((-1)%Z, (a, (b, (c, d)), nR p))); [ apply trans_eq with (Qhomographic_sign a b c d (nR p) H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption | elim (sg_tuple_equal (-1) na nb nc nd np (-1) a b c d (nR p) H6); intros _ ((H8, (H9, (H10, H11))), H12); repeat match goal with | id1:(?X1 = ?X2) |- ?X3 => rewrite id1 end; case (inside_interval_2_inf _ _ H_inside_2); intros (Ho1, Ho2); [ left; split; [ apply Zsgn_19 | apply Zsgn_20 ] | right; split; [ apply Zsgn_20 | apply Zsgn_19 ] ]; assumption ]. generalize (Qhomographic_sign_nR_10 a b c d (nR p) p (Qhomographic_signok_2 c d p H_Qhomographic_sg_denom_nonzero) H_Qhomographic_sg_denom_nonzero Hb Hd H_inside_1 H_inside_2); intro; apply (sg_neg_1 a (a + b)%Z c (c + d)%Z p (Qhomographic_signok_2 c d p H_Qhomographic_sg_denom_nonzero) na nb nc nd np); apply trans_eq with (Qhomographic_sign a b c d (nR p) H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption. case (Z_zerop b); intro Hb. case (Z_zerop d); intro Hd. generalize (Qhomographic_sign_dL_1 a b c d (dL p) p H_Qhomographic_sg_denom_nonzero (refl_equal (dL p)) Hb Hd); intro; assert (H6 : ((-1)%Z, (na, (nb, (nc, nd)), np)) = ((Z.sgn a * Z.sgn c)%Z, (a, (b, (c, d)), dL p))); [ apply trans_eq with (Qhomographic_sign a b c d (dL p) H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption | elim (sg_tuple_equal (-1) na nb nc nd np (Z.sgn a * Z.sgn c) a b c d (dL p) H6); intros H_ac ((H8, (H9, (H10, H11))), H12); repeat match goal with | id1:(?X1 = ?X2) |- ?X3 => rewrite id1 end; repeat rewrite Zplus_0_r; apply Zsgn_17; rewrite Zsgn_15; symmetry in |- *; assumption ]. case (Z_lt_dec 0 o2); intros Ho2. generalize (Qhomographic_sign_dL_2 a b c d (dL p) p H_Qhomographic_sg_denom_nonzero (refl_equal (dL p)) Hb Hd Ho2); intro; assert (H6 : ((-1)%Z, (na, (nb, (nc, nd)), np)) = (Z.sgn a, (a, (b, (c, d)), dL p))); [ apply trans_eq with (Qhomographic_sign a b c d (dL p) H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption | elim (sg_tuple_equal (-1) na nb nc nd np (Z.sgn a) a b c d (dL p) H6); intros H_a ((H8, (H9, (H10, H11))), H12); repeat match goal with | id1:(?X1 = ?X2) |- ?X3 => rewrite id1 end; repeat rewrite Zplus_0_r; right; split; [ apply Zsgn_10; symmetry in |- * | apply Zsgn_19 ]; assumption ]. case (Z_lt_dec o2 0); intros Ho2'. generalize (Qhomographic_sign_dL_3 a b c d (dL p) p H_Qhomographic_sg_denom_nonzero (refl_equal (dL p)) Hb Hd Ho2 Ho2'); intro; assert (H6 : ((-1)%Z, (na, (nb, (nc, nd)), np)) = ((- Z.sgn a)%Z, (a, (b, (c, d)), dL p))); [ apply trans_eq with (Qhomographic_sign a b c d (dL p) H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption | elim (sg_tuple_equal (-1) na nb nc nd np (- Z.sgn a) a b c d (dL p) H6); intros H_a ((H8, (H9, (H10, H11))), H12); repeat match goal with | id1:(?X1 = ?X2) |- ?X3 => rewrite id1 end; repeat rewrite Zplus_0_r; left; split; [ apply Zsgn_9; symmetry in |- *; apply Z.opp_inj | apply Zsgn_20 ]; assumption ]. generalize (Qhomographic_sign_dL_4 a b c d (dL p) p (Qhomographic_signok_3 c d p H_Qhomographic_sg_denom_nonzero) H_Qhomographic_sg_denom_nonzero Hb Hd Ho2 Ho2'); intro; apply (sg_neg_1 (a + b)%Z b (c + d)%Z d p (Qhomographic_signok_3 c d p H_Qhomographic_sg_denom_nonzero) na nb nc nd np); apply trans_eq with (Qhomographic_sign a b c d (dL p) H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption. case (Z_zerop d); intro Hd. case (Z_lt_dec 0 o1); intro Ho1. generalize (Qhomographic_sign_dL_5 a b c d (dL p) p H_Qhomographic_sg_denom_nonzero (refl_equal (dL p)) Hb Hd Ho1); intro; assert (H6 : ((-1)%Z, (na, (nb, (nc, nd)), np)) = (Z.sgn c, (a, (b, (c, d)), dL p))); [ apply trans_eq with (Qhomographic_sign a b c d (dL p) H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption | elim (sg_tuple_equal (-1) na nb nc nd np (Z.sgn c) a b c d (dL p) H6); intros H_a ((H8, (H9, (H10, H11))), H12); repeat match goal with | id1:(?X1 = ?X2) |- ?X3 => rewrite id1 end; repeat rewrite Zplus_0_r; left; split; [ apply Zsgn_19 | apply Zsgn_10; symmetry in |- * ]; assumption ]. case (Z_lt_dec o1 0); intros Ho1'. generalize (Qhomographic_sign_dL_6 a b c d (dL p) p H_Qhomographic_sg_denom_nonzero (refl_equal (dL p)) Hb Hd Ho1 Ho1'); intro; assert (H6 : ((-1)%Z, (na, (nb, (nc, nd)), np)) = ((- Z.sgn c)%Z, (a, (b, (c, d)), dL p))); [ apply trans_eq with (Qhomographic_sign a b c d (dL p) H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption | elim (sg_tuple_equal (-1) na nb nc nd np (- Z.sgn c) a b c d (dL p) H6); intros H_a ((H8, (H9, (H10, H11))), H12); repeat match goal with | id1:(?X1 = ?X2) |- ?X3 => rewrite id1 end; repeat rewrite Zplus_0_r; right; split; [ apply Zsgn_20 | apply Zsgn_9; symmetry in |- *; apply Z.opp_inj ]; assumption ]. generalize (Qhomographic_sign_dL_7 a b c d (dL p) p (Qhomographic_signok_3 c d p H_Qhomographic_sg_denom_nonzero) H_Qhomographic_sg_denom_nonzero Hb Hd Ho1 Ho1'); intro; apply (sg_neg_1 (a + b)%Z b (c + d)%Z d p (Qhomographic_signok_3 c d p H_Qhomographic_sg_denom_nonzero) na nb nc nd np); apply trans_eq with (Qhomographic_sign a b c d (dL p) H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption. case (inside_interval_1_dec_inf o1 o2); intro H_inside_1. generalize (Qhomographic_sign_dL_8 a b c d (dL p) p H_Qhomographic_sg_denom_nonzero (refl_equal (dL p)) Hb Hd H_inside_1); intro; assert (H6 : ((-1)%Z, (na, (nb, (nc, nd)), np)) = (1%Z, (a, (b, (c, d)), dL p))); [ apply trans_eq with (Qhomographic_sign a b c d (dL p) H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption | elim (sg_tuple_equal (-1) na nb nc nd np 1 a b c d (dL p) H6); intros hl H_rest; discriminate hl ]. case (inside_interval_2_dec_inf o1 o2); intro H_inside_2. generalize (Qhomographic_sign_dL_9 a b c d (dL p) p H_Qhomographic_sg_denom_nonzero (refl_equal (dL p)) Hb Hd H_inside_1 H_inside_2); intro; assert (H6 : ((-1)%Z, (na, (nb, (nc, nd)), np)) = ((-1)%Z, (a, (b, (c, d)), dL p))); [ apply trans_eq with (Qhomographic_sign a b c d (dL p) H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption | elim (sg_tuple_equal (-1) na nb nc nd np (-1) a b c d (dL p) H6); intros _ ((H8, (H9, (H10, H11))), H12); repeat match goal with | id1:(?X1 = ?X2) |- ?X3 => rewrite id1 end; case (inside_interval_2_inf _ _ H_inside_2); intros (Ho1, Ho2); [ left; split; [ apply Zsgn_19 | apply Zsgn_20 ] | right; split; [ apply Zsgn_20 | apply Zsgn_19 ] ]; assumption ]. generalize (Qhomographic_sign_dL_10 a b c d (dL p) p (Qhomographic_signok_3 c d p H_Qhomographic_sg_denom_nonzero) H_Qhomographic_sg_denom_nonzero Hb Hd H_inside_1 H_inside_2); intro; apply (sg_neg_1 (a + b)%Z b (c + d)%Z d p (Qhomographic_signok_3 c d p H_Qhomographic_sg_denom_nonzero) na nb nc nd np); apply trans_eq with (Qhomographic_sign a b c d (dL p) H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption. case (Z_zerop (Z.sgn (a + b))); intro Hab. apply False_rec; generalize (sg_One_2 a b c d One H_Qhomographic_sg_denom_nonzero (refl_equal One) Hab); intro; assert (H2 : ((-1)%Z, (na, (nb, (nc, nd)), np)) = (0%Z, (a, (b, (c, d)), One))); [ apply trans_eq with (Qhomographic_sign a b c d One H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption | elim (sg_tuple_equal (-1) na nb nc nd np 0 a b c d One H2); intros H3 H4; discriminate H3 ]. case (Z.eq_dec (Z.sgn (a + b)) (Z.sgn (c + d))); intro Habcd. generalize (sg_One_3 a b c d One H_Qhomographic_sg_denom_nonzero (refl_equal One) Hab Habcd); intro; assert (H2 : ((-1)%Z, (na, (nb, (nc, nd)), np)) = (1%Z, (a, (b, (c, d)), One))); [ apply trans_eq with (Qhomographic_sign a b c d One H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption | elim (sg_tuple_equal (-1) na nb nc nd np 1 a b c d One H2); intros H3 H4; discriminate H3 ]. generalize (sg_One_4 a b c d One H_Qhomographic_sg_denom_nonzero (refl_equal One) Hab Habcd); intro; assert (H2 : ((-1)%Z, (na, (nb, (nc, nd)), np)) = ((-1)%Z, (a, (b, (c, d)), One))); [ apply trans_eq with (Qhomographic_sign a b c d One H_Qhomographic_sg_denom_nonzero); assumption || symmetry in |- *; assumption | elim (sg_tuple_equal (-1) na nb nc nd np (-1) a b c d One H2); intros _ ((H8, (H9, (H10, H11))), H12); repeat match goal with | id1:(?X1 = ?X2) |- ?X3 => rewrite id1 end ]. case (not_Zeq_inf (Z.sgn (a + b)) 0 Hab); intro Hab'; [ right; split; [ apply Zsgn_11; assumption | apply Zsgn_12 ]; generalize (Zsgn_1' (c + d)); intros [[Hcd| Hcd]| Hcd]; [ apply False_ind; apply (Qhomographic_signok_1 c d H_Qhomographic_sg_denom_nonzero); apply Zsgn_2 | rewrite Hcd; constructor | apply False_ind; apply Habcd; rewrite Hcd; apply Zsgn_8; apply Zsgn_11 ]; assumption | left; split; [ apply Zsgn_12; assumption | apply Zsgn_11 ]; generalize (Zsgn_1' (c + d)); intros [[Hcd| Hcd]| Hcd]; [ apply False_ind; apply (Qhomographic_signok_1 c d H_Qhomographic_sg_denom_nonzero); apply Zsgn_2 | apply False_ind; apply Habcd; rewrite Hcd; apply Zsgn_7; apply Z.lt_gt; apply Zsgn_12 | rewrite Hcd; constructor ]; assumption ]. Qed.
imports: Coq(ZArithRing) QArithSternBrocot(Zaux)