proposition: Lemma sg_sign : forall (a b c d : Z) (qp : Qpositive) (H_Qhomographic_sg_denom_nonzero : Qhomographic_sg_denom_nonzero c d qp), let (l1, L2) := Qhomographic_sign a b c d qp H_Qhomographic_sg_denom_nonzero in {l1 = 0%Z} + {l1 = 1%Z} + {l1 = (-1)%Z}.
proof: Proof. fix sg_sign 5. intros. let T_local := (case (Z_zerop b); intro Hb; [ case (Z_zerop d); intro Hd; [ match goal with | id1:(?X1 ?X2 ?X3 (nR ?X4)) |- ?X5 => rewrite (Qhomographic_sign_nR_1 a b c d (nR q) q H_Qhomographic_sg_denom_nonzero (refl_equal (nR q)) Hb Hd) | id1:(?X1 ?X2 ?X3 (dL ?X4)) |- ?X5 => rewrite (Qhomographic_sign_dL_1 a b c d (dL q) q H_Qhomographic_sg_denom_nonzero (refl_equal (dL q)) Hb Hd) end; generalize a c; intros [|pa|pa] [| pc| pc]; simpl in |- *; first [ right; reflexivity | left; left; reflexivity | left; right; reflexivity ] | case (Z_lt_dec 0 (outside_interval c d)); intros Ho2; [ match goal with | id1:(?X1 ?X2 ?X3 (nR ?X4)) |- ?X5 => rewrite (Qhomographic_sign_nR_2 a b c d (nR q) q H_Qhomographic_sg_denom_nonzero (refl_equal (nR q)) Hb Hd Ho2) | id1:(?X1 ?X2 ?X3 (dL ?X4)) |- ?X5 => rewrite (Qhomographic_sign_dL_2 a b c d (dL q) q H_Qhomographic_sg_denom_nonzero (refl_equal (dL q)) Hb Hd Ho2) end; generalize a; intros [| pa| pa]; simpl in |- *; first [ right; reflexivity | left; left; reflexivity | left; right; reflexivity ] | case (Z_lt_dec (outside_interval c d) 0); intros Ho2'; [ match goal with | id1:(?X1 ?X2 ?X3 (nR ?X4)) |- ?X5 => rewrite (Qhomographic_sign_nR_3 a b c d (nR q) q H_Qhomographic_sg_denom_nonzero (refl_equal (nR q)) Hb Hd Ho2 Ho2') | id1:(?X1 ?X2 ?X3 (dL ?X4)) |- ?X5 => rewrite (Qhomographic_sign_dL_3 a b c d (dL q) q H_Qhomographic_sg_denom_nonzero (refl_equal (dL q)) Hb Hd Ho2 Ho2') end; generalize a; intros [| pa| pa]; simpl in |- *; first [ right; reflexivity | left; left; reflexivity | left; right; reflexivity ] | match goal with | id1:(?X1 ?X2 ?X3 (nR ?X4)) |- ?X5 => rewrite (Qhomographic_sign_nR_4 a b c d (nR q) q (Qhomographic_signok_2 c d q H_Qhomographic_sg_denom_nonzero) H_Qhomographic_sg_denom_nonzero Hb Hd Ho2 Ho2') | id1:(?X1 ?X2 ?X3 (dL ?X4)) |- ?X5 => rewrite (Qhomographic_sign_dL_4 a b c d (dL q) q (Qhomographic_signok_3 c d q H_Qhomographic_sg_denom_nonzero) H_Qhomographic_sg_denom_nonzero Hb Hd Ho2 Ho2') end; apply sg_sign ] ] ] | case (Z_zerop d); intro Hd; [ case (Z_lt_dec 0 (outside_interval a b)); intros Ho1; [ match goal with | id1:(?X1 ?X2 ?X3 (nR ?X4)) |- ?X5 => rewrite (Qhomographic_sign_nR_5 a b c d (nR q) q H_Qhomographic_sg_denom_nonzero (refl_equal (nR q)) Hb Hd Ho1) | id1:(?X1 ?X2 ?X3 (dL ?X4)) |- ?X5 => rewrite (Qhomographic_sign_dL_5 a b c d (dL q) q H_Qhomographic_sg_denom_nonzero (refl_equal (dL q)) Hb Hd Ho1) end; generalize c; intros [| pc| pc]; simpl in |- *; first [ right; reflexivity | left; left; reflexivity | left; right; reflexivity ] | case (Z_lt_dec (outside_interval a b) 0); intros Ho1'; [ match goal with | id1:(?X1 ?X2 ?X3 (nR ?X4)) |- ?X5 => rewrite (Qhomographic_sign_nR_6 a b c d (nR q) q H_Qhomographic_sg_denom_nonzero (refl_equal (nR q)) Hb Hd Ho1 Ho1') | id1:(?X1 ?X2 ?X3 (dL ?X4)) |- ?X5 => rewrite (Qhomographic_sign_dL_6 a b c d (dL q) q H_Qhomographic_sg_denom_nonzero (refl_equal (dL q)) Hb Hd Ho1 Ho1') end; generalize c; intros [| pc| pc]; simpl in |- *; first [ right; reflexivity | left; left; reflexivity | left; right; reflexivity ] | match goal with | id1:(?X1 ?X2 ?X3 (nR ?X4)) |- ?X5 => rewrite (Qhomographic_sign_nR_7 a b c d (nR q) q (Qhomographic_signok_2 c d q H_Qhomographic_sg_denom_nonzero) H_Qhomographic_sg_denom_nonzero Hb Hd Ho1 Ho1') | id1:(?X1 ?X2 ?X3 (dL ?X4)) |- ?X5 => rewrite (Qhomographic_sign_dL_7 a b c d (dL q) q (Qhomographic_signok_3 c d q H_Qhomographic_sg_denom_nonzero) H_Qhomographic_sg_denom_nonzero Hb Hd Ho1 Ho1') end; apply sg_sign ] ] | case (inside_interval_1_dec_inf (outside_interval a b) (outside_interval c d)); intros H_inside_1; [ match goal with | id1:(?X1 ?X2 ?X3 (nR ?X4)) |- ?X5 => rewrite (Qhomographic_sign_nR_8 a b c d (nR q) q H_Qhomographic_sg_denom_nonzero (refl_equal (nR q)) Hb Hd H_inside_1) | id1:(?X1 ?X2 ?X3 (dL ?X4)) |- ?X5 => rewrite (Qhomographic_sign_dL_8 a b c d (dL q) q H_Qhomographic_sg_denom_nonzero (refl_equal (dL q)) Hb Hd H_inside_1) end; first [ right; reflexivity | left; left; reflexivity | left; right; reflexivity ] | case (inside_interval_2_dec_inf (outside_interval a b) (outside_interval c d)); intros H_inside_2; [ match goal with | id1:(?X1 ?X2 ?X3 (nR ?X4)) |- ?X5 => rewrite (Qhomographic_sign_nR_9 a b c d (nR q) q H_Qhomographic_sg_denom_nonzero (refl_equal (nR q)) Hb Hd H_inside_1 H_inside_2) | id1:(?X1 ?X2 ?X3 (dL ?X4)) |- ?X5 => rewrite (Qhomographic_sign_dL_9 a b c d (dL q) q H_Qhomographic_sg_denom_nonzero (refl_equal (dL q)) Hb Hd H_inside_1 H_inside_2) end; first [ right; reflexivity | left; left; reflexivity | left; right; reflexivity ] | match goal with | id1:(?X1 ?X2 ?X3 (nR ?X4)) |- ?X5 => rewrite (Qhomographic_sign_nR_10 a b c d (nR q) q (Qhomographic_signok_2 c d q H_Qhomographic_sg_denom_nonzero) H_Qhomographic_sg_denom_nonzero Hb Hd H_inside_1 H_inside_2) | id1:(?X1 ?X2 ?X3 (dL ?X4)) |- ?X5 => rewrite (Qhomographic_sign_dL_10 a b c d (dL q) q (Qhomographic_signok_3 c d q H_Qhomographic_sg_denom_nonzero) H_Qhomographic_sg_denom_nonzero Hb Hd H_inside_1 H_inside_2) end; apply sg_sign ] ] ] ]) in (destruct qp as [q| q| ]; [ T_local | T_local | case (Z.eq_dec (Z.sgn (a + b)) 0); intro H_ab; [ rewrite (sg_One_2 a b c d One H_Qhomographic_sg_denom_nonzero (refl_equal One) H_ab) | case (Z.eq_dec (Z.sgn (a + b)) (Z.sgn (c + d))); intro H_ab_cd; [ rewrite (sg_One_3 a b c d One H_Qhomographic_sg_denom_nonzero (refl_equal One) H_ab H_ab_cd) | rewrite (sg_One_4 a b c d One H_Qhomographic_sg_denom_nonzero (refl_equal One) H_ab H_ab_cd) ] ]; first [ right; reflexivity | left; left; reflexivity | left; right; reflexivity ] ]). Defined.
imports: Coq(ZArithRing)