proposition: Lemma homographic_sign : forall (a b c d : Z) (p : Qpositive) (H_Qhomographic_sg_denom_nonzero : Qhomographic_sg_denom_nonzero c d p), h_sign a b c d p H_Qhomographic_sg_denom_nonzero = Qsgn (spec_Qhomographic_Qpositive_to_Q a b c d p).
proof: Proof. intros a b c d p H_Qhomographic_sg_denom_nonzero. unfold h_sign in |- *. functional induction (Qhomographic_sign a b c d p H_Qhomographic_sg_denom_nonzero). unfold spec_Qhomographic_Qpositive_to_Q in |- *. simpl in |- *. transitivity (Qsgn (Qmult (Qmult a (Qpos (nR q))) (Qinv (Qmult c (Qpos (nR q)))))). repeat rewrite Qsgn_15. rewrite Qsgn_28. rewrite Qsgn_15. simpl in |- *. repeat rewrite Qsgn_29. abstract ring. apply f_equal with Q. field. split. discriminate. intro; generalize (Qhomographic_sg_denom_nonzero_nonzero_3 c 0 (nR q) H_Qhomographic_sg_denom_nonzero); intros [H_| H_]; apply H_; clear H_; [ apply eq_Z_to_Q; assumption | reflexivity]. unfold spec_Qhomographic_Qpositive_to_Q in |- *. clear e3 e1 e2; simpl in |- *. transitivity (Qsgn (Qmult (Qmult a (Qpos (nR q))) (Qinv (Qplus (Qmult c (Qpos (nR q))) d)))). repeat rewrite Qsgn_15. rewrite Qsgn_28. simpl in |- *. generalize (Zsgn_21 _ _ l) (Zsgn_23 _ _ l) (Zsgn_19 _ _ l); intros Hc_nonneg Hd_nonneg Hcd_pos. replace (Qsgn (Qplus (Qmult c (Qpos (nR q))) d)) with 1%Z. rewrite Qsgn_29. abstract auto with zarith. symmetry in |- *. apply Qsgn_7. generalize (Zlt_cotrans_pos _ _ Hcd_pos); intros [Hc| Hd]; [ apply Qlt_le_reg_pos; [ apply Qsgn_9; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonneg; assumption ] | apply Qle_lt_reg_pos; [ apply Qle_mult_nonneg_nonneg; [ apply Z_to_Q_nonneg; assumption | auto with * ] | apply Z_to_Q_pos; assumption ] ]. apply f_equal with Q. apply f_equal2 with Q Q; [ field | reflexivity ]. unfold spec_Qhomographic_Qpositive_to_Q in |- *; clear e4 e1 e2 e3; simpl in |- *. transitivity (Qsgn (Qmult (Qmult a (Qpos (nR q))) (Qinv (Qplus (Qmult c (Qpos (nR q))) d)))). repeat rewrite Qsgn_15. rewrite Qsgn_28. simpl in |- *. generalize (Zsgn_22 _ _ l) (Zsgn_24 _ _ l) (Zsgn_20 _ _ l); intros Hc_nonpos Hd_nonpos Hcd_neg. replace (Qsgn (Qplus (Qmult c (Qpos (nR q))) d)) with (-1)%Z. rewrite Qsgn_29. abstract auto with zarith. symmetry in |- *. apply Qsgn_8. generalize (Zlt_cotrans_neg _ _ Hcd_neg); intros [Hc| Hd]; [ apply Qlt_le_reg_neg; [ apply Qsgn_10; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonpos; assumption ] | apply Qle_lt_reg_neg; [ apply Qle_mult_nonpos_pos; [ apply Z_to_Q_nonpos; assumption | auto with * ] | apply Z_to_Q_neg; assumption ] ]. apply f_equal with Q. apply f_equal2 with Q Q; [ field | reflexivity ]. clear e4 e1 e2 e3; rewrite spec_Qhomographic_Qpositive_to_Q_nR; rewrite IHp0; reflexivity. unfold spec_Qhomographic_Qpositive_to_Q in |- *; clear e3 e0 e2. simpl in |- *. transitivity (Qsgn (Qmult (Qplus (Qmult a (Qpos (nR q))) b) (Qinv (Qmult c (Qpos (nR q)))))). repeat rewrite Qsgn_15. rewrite Qsgn_28. rewrite Qsgn_15. simpl in |- *. generalize (Zsgn_21 _ _ l) (Zsgn_23 _ _ l) (Zsgn_19 _ _ l); intros Ha_nonneg Hb_nonneg Hab_pos. replace (Qsgn (Qplus (Qmult a (Qpos (nR q))) b)) with 1%Z. rewrite Qsgn_29. abstract auto with zarith. symmetry in |- *. apply Qsgn_7. generalize (Zlt_cotrans_pos _ _ Hab_pos); intros [Ha_| Hb_]; [ apply Qlt_le_reg_pos; [ apply Qsgn_9; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonneg; assumption ] | apply Qle_lt_reg_pos; [ apply Qle_mult_nonneg_nonneg; [ apply Z_to_Q_nonneg; assumption | auto with * ] | apply Z_to_Q_pos; assumption ] ]. apply f_equal with Q. apply f_equal2 with Q Q; [ reflexivity | apply f_equal with Q; abstract ring ]. unfold spec_Qhomographic_Qpositive_to_Q in |- *; clear e4 e0 e2 e3; simpl in |- *. transitivity (Qsgn (Qmult (Qplus (Qmult a (Qpos (nR q))) b) (Qinv (Qmult c (Qpos (nR q)))))). repeat rewrite Qsgn_15. rewrite Qsgn_28. rewrite Qsgn_15. simpl in |- *. generalize (Zsgn_22 _ _ l) (Zsgn_24 _ _ l) (Zsgn_20 _ _ l); intros Ha_nonpos Hb_nonpos Hab_neg. replace (Qsgn (Qplus (Qmult a (Qpos (nR q))) b)) with (-1)%Z. rewrite Qsgn_29. abstract auto with zarith. symmetry in |- *. apply Qsgn_8. generalize (Zlt_cotrans_neg _ _ Hab_neg); intros [Ha_| Hb_]; [ apply Qlt_le_reg_neg; [ apply Qsgn_10; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonpos; assumption ] | apply Qle_lt_reg_neg; [ apply Qle_mult_nonpos_pos; [ apply Z_to_Q_nonpos; assumption | auto with * ] | apply Z_to_Q_neg; assumption ] ]. apply f_equal with Q. apply f_equal2 with Q Q; [ reflexivity | apply f_equal with Q; abstract ring ]. clear e4 e0 e2 e3 ; rewrite spec_Qhomographic_Qpositive_to_Q_nR; rewrite IHp0; reflexivity. unfold spec_Qhomographic_Qpositive_to_Q in |- *; clear e0 e1 e2. repeat rewrite Qsgn_15. rewrite Qsgn_28. case (inside_interval_1_inf _ _ i); clear i; intros (Hab, Hcd); repeat match goal with | id1:(0 < outside_interval _ _)%Z |- _ => generalize (Zsgn_21 _ _ id1) (Zsgn_23 _ _ id1) (Zsgn_19 _ _ id1); clear id1 | id1:(outside_interval _ _ < 0)%Z |- _ => generalize (Zsgn_22 _ _ id1) (Zsgn_24 _ _ id1) (Zsgn_20 _ _ id1); clear id1 end; intros Ha_ Hb_ Hab_ Hc_ Hd_ Hcd_. replace (Qsgn (Qplus (Qmult a (Qpos (nR q))) b)) with 1%Z. replace (Qsgn (Qplus (Qmult c (Qpos (nR q))) d)) with 1%Z. abstract auto with zarith. symmetry in |- *; apply Qsgn_7; generalize (Zlt_cotrans_pos _ _ Hcd_); intros [Hc_1| Hd_1]; [ apply Qlt_le_reg_pos; [ apply Qsgn_9; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonneg; assumption ] | apply Qle_lt_reg_pos; [ apply Qle_mult_nonneg_nonneg; [ apply Z_to_Q_nonneg; assumption | auto with * ] | apply Z_to_Q_pos; assumption ] ]. symmetry in |- *; apply Qsgn_7; generalize (Zlt_cotrans_pos _ _ Hab_); intros [Ha_1| Hb_1]; [ apply Qlt_le_reg_pos; [ apply Qsgn_9; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonneg; assumption ] | apply Qle_lt_reg_pos; [ apply Qle_mult_nonneg_nonneg; [ apply Z_to_Q_nonneg; assumption | auto with * ] | apply Z_to_Q_pos; assumption ] ]. replace (Qsgn (Qplus (Qmult a (Qpos (nR q))) b)) with (-1)%Z. replace (Qsgn (Qplus (Qmult c (Qpos (nR q))) d)) with (-1)%Z. abstract auto with zarith. symmetry in |- *; apply Qsgn_8; generalize (Zlt_cotrans_neg _ _ Hcd_); intros [Hc_1| Hd_1]; [ apply Qlt_le_reg_neg; [ apply Qsgn_10; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonpos; assumption ] | apply Qle_lt_reg_neg; [ apply Qle_mult_nonpos_pos; [ apply Z_to_Q_nonpos; assumption | auto with * ] | apply Z_to_Q_neg; assumption ] ]. symmetry in |- *; apply Qsgn_8; generalize (Zlt_cotrans_neg _ _ Hab_); intros [Ha_1| Hb_1]; [ apply Qlt_le_reg_neg; [ apply Qsgn_10; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonpos; assumption ] | apply Qle_lt_reg_neg; [ apply Qle_mult_nonpos_pos; [ apply Z_to_Q_nonpos; assumption | auto with * ] | apply Z_to_Q_neg; assumption ] ]. unfold spec_Qhomographic_Qpositive_to_Q in |- *; clear e1 e2 e3. repeat rewrite Qsgn_15. rewrite Qsgn_28. case (inside_interval_2_inf _ _ i); clear i; intros (Hab, Hcd); repeat match goal with | id1:(0 < outside_interval _ _)%Z |- _ => generalize (Zsgn_21 _ _ id1) (Zsgn_23 _ _ id1) (Zsgn_19 _ _ id1); clear id1 | id1:(outside_interval _ _ < 0)%Z |- _ => generalize (Zsgn_22 _ _ id1) (Zsgn_24 _ _ id1) (Zsgn_20 _ _ id1); clear id1 end. intros Hc_ Hd_ Hcd_ Ha_ Hb_ Hab_. replace (Qsgn (Qplus (Qmult a (Qpos (nR q))) b)) with 1%Z. replace (Qsgn (Qplus (Qmult c (Qpos (nR q))) d)) with (-1)%Z. abstract auto with zarith. symmetry in |- *; apply Qsgn_8; generalize (Zlt_cotrans_neg _ _ Hcd_); intros [Hc_1| Hd_1]; [ apply Qlt_le_reg_neg; [ apply Qsgn_10; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonpos; assumption ] | apply Qle_lt_reg_neg; [ apply Qle_mult_nonpos_pos; [ apply Z_to_Q_nonpos; assumption | auto with * ] | apply Z_to_Q_neg; assumption ] ]. symmetry in |- *; apply Qsgn_7; generalize (Zlt_cotrans_pos _ _ Hab_); intros [Ha_1| Hb_1]; [ apply Qlt_le_reg_pos; [ apply Qsgn_9; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonneg; assumption ] | apply Qle_lt_reg_pos; [ apply Qle_mult_nonneg_nonneg; [ apply Z_to_Q_nonneg; assumption | auto with * ] | apply Z_to_Q_pos; assumption ] ]. intros Ha_ Hb_ Hab_ Hc_ Hd_ Hcd_. replace (Qsgn (Qplus (Qmult a (Qpos (nR q))) b)) with (-1)%Z. replace (Qsgn (Qplus (Qmult c (Qpos (nR q))) d)) with 1%Z. abstract auto with zarith. symmetry in |- *; apply Qsgn_7; generalize (Zlt_cotrans_pos _ _ Hcd_); intros [Hc_1| Hd_1]; [ apply Qlt_le_reg_pos; [ apply Qsgn_9; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonneg; assumption ] | apply Qle_lt_reg_pos; [ apply Qle_mult_nonneg_nonneg; [ apply Z_to_Q_nonneg; assumption | auto with * ] | apply Z_to_Q_pos; assumption ] ]. symmetry in |- *; apply Qsgn_8; generalize (Zlt_cotrans_neg _ _ Hab_); intros [Ha_1| Hb_1]; [ apply Qlt_le_reg_neg; [ apply Qsgn_10; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonpos; assumption ] | apply Qle_lt_reg_neg; [ apply Qle_mult_nonpos_pos; [ apply Z_to_Q_nonpos; assumption | auto with * ] | apply Z_to_Q_neg; assumption ] ]. clear e3 e0 e1 e2; rewrite spec_Qhomographic_Qpositive_to_Q_nR; rewrite IHp0; reflexivity. unfold spec_Qhomographic_Qpositive_to_Q in |- *; clear e1 e3. simpl in |- *. transitivity (Qsgn (Qmult (Qmult a (Qpos (dL q))) (Qinv (Qmult c (Qpos (dL q)))))). repeat rewrite Qsgn_15. rewrite Qsgn_28. rewrite Qsgn_15. simpl in |- *. repeat rewrite Qsgn_29. abstract ring. apply f_equal with Q. field. split. discriminate. intro; generalize (Qhomographic_sg_denom_nonzero_nonzero_3 c 0 (dL q) H_Qhomographic_sg_denom_nonzero); intros [H_| H_]; apply H_; clear H_; [ apply eq_Z_to_Q; assumption | reflexivity]. unfold spec_Qhomographic_Qpositive_to_Q in |- *. clear e2 e1 e3; simpl in |- *. transitivity (Qsgn (Qmult (Qmult a (Qpos (dL q))) (Qinv (Qplus (Qmult c (Qpos (dL q))) d)))). repeat rewrite Qsgn_15. rewrite Qsgn_28. simpl in |- *. generalize (Zsgn_21 _ _ l) (Zsgn_23 _ _ l) (Zsgn_19 _ _ l); intros Hc_nonneg Hd_nonneg Hcd_pos. replace (Qsgn (Qplus (Qmult c (Qpos (dL q))) d)) with 1%Z. rewrite Qsgn_29. abstract auto with zarith. symmetry in |- *. apply Qsgn_7. generalize (Zlt_cotrans_pos _ _ Hcd_pos); intros [Hc| Hd]; [ apply Qlt_le_reg_pos; [ apply Qsgn_9; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonneg; assumption ] | apply Qle_lt_reg_pos; [ apply Qle_mult_nonneg_nonneg; [ apply Z_to_Q_nonneg; assumption | auto with * ] | apply Z_to_Q_pos; assumption ] ]. apply f_equal with Q. apply f_equal2 with Q Q; [ field | reflexivity ]. unfold spec_Qhomographic_Qpositive_to_Q in |- *; clear e4 e1 e2 e3; simpl in |- *. transitivity (Qsgn (Qmult (Qmult a (Qpos (dL q))) (Qinv (Qplus (Qmult c (Qpos (dL q))) d)))). repeat rewrite Qsgn_15. rewrite Qsgn_28. simpl in |- *. generalize (Zsgn_22 _ _ l) (Zsgn_24 _ _ l) (Zsgn_20 _ _ l); intros Hc_nonpos Hd_nonpos Hcd_neg. replace (Qsgn (Qplus (Qmult c (Qpos (dL q))) d)) with (-1)%Z. rewrite Qsgn_29. abstract auto with zarith. symmetry in |- *. apply Qsgn_8. generalize (Zlt_cotrans_neg _ _ Hcd_neg); intros [Hc| Hd]; [ apply Qlt_le_reg_neg; [ apply Qsgn_10; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonpos; assumption ] | apply Qle_lt_reg_neg; [ apply Qle_mult_nonpos_pos; [ apply Z_to_Q_nonpos; assumption | auto with * ] | apply Z_to_Q_neg; assumption ] ]. apply f_equal with Q. apply f_equal2 with Q Q; [ field | reflexivity ]. clear e4 e1 e2 e3; rewrite spec_Qhomographic_Qpositive_to_Q_dL; rewrite IHp0; reflexivity. unfold spec_Qhomographic_Qpositive_to_Q in |- *; clear e3 e0 e2 . simpl in |- *. transitivity (Qsgn (Qmult (Qplus (Qmult a (Qpos (dL q))) b) (Qinv (Qmult c (Qpos (dL q)))))). repeat rewrite Qsgn_15. rewrite Qsgn_28. rewrite Qsgn_15. simpl in |- *. generalize (Zsgn_21 _ _ l) (Zsgn_23 _ _ l) (Zsgn_19 _ _ l); intros Ha_nonneg Hb_nonneg Hab_pos. replace (Qsgn (Qplus (Qmult a (Qpos (dL q))) b)) with 1%Z. rewrite Qsgn_29. abstract auto with zarith. symmetry in |- *. apply Qsgn_7. generalize (Zlt_cotrans_pos _ _ Hab_pos); intros [Ha_| Hb_]; [ apply Qlt_le_reg_pos; [ apply Qsgn_9; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonneg; assumption ] | apply Qle_lt_reg_pos; [ apply Qle_mult_nonneg_nonneg; [ apply Z_to_Q_nonneg; assumption | auto with * ] | apply Z_to_Q_pos; assumption ] ]. apply f_equal with Q. apply f_equal2 with Q Q; [ reflexivity | apply f_equal with Q; abstract ring ]. unfold spec_Qhomographic_Qpositive_to_Q in |- *; clear e4 e0 e2 e3; simpl in |- *. transitivity (Qsgn (Qmult (Qplus (Qmult a (Qpos (dL q))) b) (Qinv (Qmult c (Qpos (dL q)))))). repeat rewrite Qsgn_15. rewrite Qsgn_28. rewrite Qsgn_15. simpl in |- *. generalize (Zsgn_22 _ _ l) (Zsgn_24 _ _ l) (Zsgn_20 _ _ l); intros Ha_nonpos Hb_nonpos Hab_neg. replace (Qsgn (Qplus (Qmult a (Qpos (dL q))) b)) with (-1)%Z. rewrite Qsgn_29. abstract auto with zarith. symmetry in |- *. apply Qsgn_8. generalize (Zlt_cotrans_neg _ _ Hab_neg); intros [Ha_| Hb_]; [ apply Qlt_le_reg_neg; [ apply Qsgn_10; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonpos; assumption ] | apply Qle_lt_reg_neg; [ apply Qle_mult_nonpos_pos; [ apply Z_to_Q_nonpos; assumption | auto with * ] | apply Z_to_Q_neg; assumption ] ]. apply f_equal with Q. apply f_equal2 with Q Q; [ reflexivity | apply f_equal with Q; abstract ring ]. clear e3 e0 e4 e2 ; rewrite spec_Qhomographic_Qpositive_to_Q_dL; rewrite IHp0; reflexivity. unfold spec_Qhomographic_Qpositive_to_Q in |- *; clear e2 e0 e1 . repeat rewrite Qsgn_15. rewrite Qsgn_28. case (inside_interval_1_inf _ _ i); clear i; intros (Hab, Hcd); repeat match goal with | id1:(0 < outside_interval _ _)%Z |- _ => generalize (Zsgn_21 _ _ id1) (Zsgn_23 _ _ id1) (Zsgn_19 _ _ id1); clear id1 | id1:(outside_interval _ _ < 0)%Z |- _ => generalize (Zsgn_22 _ _ id1) (Zsgn_24 _ _ id1) (Zsgn_20 _ _ id1); clear id1 end; intros Ha_ Hb_ Hab_ Hc_ Hd_ Hcd_. replace (Qsgn (Qplus (Qmult a (Qpos (dL q))) b)) with 1%Z. replace (Qsgn (Qplus (Qmult c (Qpos (dL q))) d)) with 1%Z. abstract auto with zarith. symmetry in |- *; apply Qsgn_7; generalize (Zlt_cotrans_pos _ _ Hcd_); intros [Hc_1| Hd_1]; [ apply Qlt_le_reg_pos; [ apply Qsgn_9; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonneg; assumption ] | apply Qle_lt_reg_pos; [ apply Qle_mult_nonneg_nonneg; [ apply Z_to_Q_nonneg; assumption | auto with * ] | apply Z_to_Q_pos; assumption ] ]. symmetry in |- *; apply Qsgn_7; generalize (Zlt_cotrans_pos _ _ Hab_); intros [Ha_1| Hb_1]; [ apply Qlt_le_reg_pos; [ apply Qsgn_9; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonneg; assumption ] | apply Qle_lt_reg_pos; [ apply Qle_mult_nonneg_nonneg; [ apply Z_to_Q_nonneg; assumption | auto with * ] | apply Z_to_Q_pos; assumption ] ]. replace (Qsgn (Qplus (Qmult a (Qpos (dL q))) b)) with (-1)%Z. replace (Qsgn (Qplus (Qmult c (Qpos (dL q))) d)) with (-1)%Z. abstract auto with zarith. symmetry in |- *; apply Qsgn_8; generalize (Zlt_cotrans_neg _ _ Hcd_); intros [Hc_1| Hd_1]; [ apply Qlt_le_reg_neg; [ apply Qsgn_10; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonpos; assumption ] | apply Qle_lt_reg_neg; [ apply Qle_mult_nonpos_pos; [ apply Z_to_Q_nonpos; assumption | auto with * ] | apply Z_to_Q_neg; assumption ] ]. symmetry in |- *; apply Qsgn_8; generalize (Zlt_cotrans_neg _ _ Hab_); intros [Ha_1| Hb_1]; [ apply Qlt_le_reg_neg; [ apply Qsgn_10; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonpos; assumption ] | apply Qle_lt_reg_neg; [ apply Qle_mult_nonpos_pos; [ apply Z_to_Q_nonpos; assumption | auto with * ] | apply Z_to_Q_neg; assumption ] ]. unfold spec_Qhomographic_Qpositive_to_Q in |- *; clear e3 e0 e1 e2. repeat rewrite Qsgn_15. rewrite Qsgn_28. case (inside_interval_2_inf _ _ i); clear i; intros (Hab, Hcd); repeat match goal with | id1:(0 < outside_interval _ _)%Z |- _ => generalize (Zsgn_21 _ _ id1) (Zsgn_23 _ _ id1) (Zsgn_19 _ _ id1); clear id1 | id1:(outside_interval _ _ < 0)%Z |- _ => generalize (Zsgn_22 _ _ id1) (Zsgn_24 _ _ id1) (Zsgn_20 _ _ id1); clear id1 end. intros Hc_ Hd_ Hcd_ Ha_ Hb_ Hab_. replace (Qsgn (Qplus (Qmult a (Qpos (dL q))) b)) with 1%Z. replace (Qsgn (Qplus (Qmult c (Qpos (dL q))) d)) with (-1)%Z. abstract auto with zarith. symmetry in |- *; apply Qsgn_8; generalize (Zlt_cotrans_neg _ _ Hcd_); intros [Hc_1| Hd_1]; [ apply Qlt_le_reg_neg; [ apply Qsgn_10; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonpos; assumption ] | apply Qle_lt_reg_neg; [ apply Qle_mult_nonpos_pos; [ apply Z_to_Q_nonpos; assumption | auto with * ] | apply Z_to_Q_neg; assumption ] ]. symmetry in |- *; apply Qsgn_7; generalize (Zlt_cotrans_pos _ _ Hab_); intros [Ha_1| Hb_1]; [ apply Qlt_le_reg_pos; [ apply Qsgn_9; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonneg; assumption ] | apply Qle_lt_reg_pos; [ apply Qle_mult_nonneg_nonneg; [ apply Z_to_Q_nonneg; assumption | auto with * ] | apply Z_to_Q_pos; assumption ] ]. intros Ha_ Hb_ Hab_ Hc_ Hd_ Hcd_. replace (Qsgn (Qplus (Qmult a (Qpos (dL q))) b)) with (-1)%Z. replace (Qsgn (Qplus (Qmult c (Qpos (dL q))) d)) with 1%Z. abstract auto with zarith. symmetry in |- *; apply Qsgn_7; generalize (Zlt_cotrans_pos _ _ Hcd_); intros [Hc_1| Hd_1]; [ apply Qlt_le_reg_pos; [ apply Qsgn_9; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonneg; assumption ] | apply Qle_lt_reg_pos; [ apply Qle_mult_nonneg_nonneg; [ apply Z_to_Q_nonneg; assumption | auto with * ] | apply Z_to_Q_pos; assumption ] ]. symmetry in |- *; apply Qsgn_8; generalize (Zlt_cotrans_neg _ _ Hab_); intros [Ha_1| Hb_1]; [ apply Qlt_le_reg_neg; [ apply Qsgn_10; rewrite Qsgn_15; simpl in |- *; rewrite Qsgn_29; rewrite Zmult_1_r; abstract auto with zarith | apply Z_to_Q_nonpos; assumption ] | apply Qle_lt_reg_neg; [ apply Qle_mult_nonpos_pos; [ apply Z_to_Q_nonpos; assumption | auto with * ] | apply Z_to_Q_neg; assumption ] ]. clear e0 e1 e2 e3; rewrite spec_Qhomographic_Qpositive_to_Q_dL; rewrite IHp0; reflexivity. unfold spec_Qhomographic_Qpositive_to_Q in |- *; clear e1. rewrite Qsgn_15. replace (Qsgn (Qplus (Qmult a (Qpos One)) b)) with 0%Z. abstract auto with zarith. rewrite Qmult_sym. rewrite Qmult_one_left. rewrite <- Z_to_Qplus. symmetry in |- *. rewrite Qsgn_29. assumption. Transparent Qone. unfold spec_Qhomographic_Qpositive_to_Q in |- *; clear e2 ; rewrite Qsgn_15; repeat rewrite Qmult_one_right; rewrite Qsgn_28; repeat rewrite <- Z_to_Qplus; repeat rewrite Qsgn_29; rewrite <- e1; rewrite <- Zsgn_15; symmetry in |- *; apply Zsgn_7'; abstract auto with zarith. unfold spec_Qhomographic_Qpositive_to_Q in |- *; clear e1 e0; abstract (rewrite Qsgn_15; repeat rewrite Qmult_one_right; rewrite Qsgn_28; repeat rewrite <- Z_to_Qplus; repeat rewrite Qsgn_29; generalize (Zsgn_3 _ (Qhomographic_signok_1 _ _ _x)); intro Hcd_; generalize (Zsgn_1' (a + b)) (Zsgn_1' (c + d)); intros [[Hab| Hab]| Hab] [[Hcd| Hcd]| Hcd]; try solve [ Falsum ]; rewrite Hab in n0; rewrite Hcd in n0; try solve [ Falsum ]; rewrite Hab; rewrite Hcd; constructor). Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)