proposition: Lemma Qquadratic_sign_equal : forall (a b c d e f g h : Z) (p1 p2 : Qpositive) (H1 H2 : Qquadratic_sg_denom_nonzero e f g h p1 p2), Qquadratic_sign a b c d e f g h p1 p2 H1 = Qquadratic_sign a b c d e f g h p1 p2 H2.
proof: Proof. intros. generalize H2 H1 a b c d. intro. elim H0 using Qquadratic_sg_denom_nonzero_inv_dep. intros. destruct p3 as [p| p| ]; rename q into s. discriminate e1. discriminate e1. destruct p0 as [p| p| ]. unfold Qquadratic_sign in |- *. assert (Qhomographic_sign (a0 + b0) (c0 + d0) (e0 + f0) (g0 + h0) (nR p) (Qquadratic_signok_0' e0 f0 g0 h0 (nR p) H3) = Qhomographic_sign (a0 + b0) (c0 + d0) (e0 + f0) (g0 + h0) (nR p) (Qquadratic_signok_0' e0 f0 g0 h0 (nR p) (Qquadratic_signok0 e0 f0 g0 h0 (nR p) One e1 s))). apply Qhomographic_sign_equal. rewrite H. reflexivity. unfold Qquadratic_sign in |- *. assert (Qhomographic_sign (a0 + b0) (c0 + d0) (e0 + f0) (g0 + h0) (dL p) (Qquadratic_signok_0' e0 f0 g0 h0 (dL p) H3) = Qhomographic_sign (a0 + b0) (c0 + d0) (e0 + f0) (g0 + h0) (dL p) (Qquadratic_signok_0' e0 f0 g0 h0 (dL p) (Qquadratic_signok0 e0 f0 g0 h0 (dL p) One e1 s))). apply Qhomographic_sign_equal. rewrite H. reflexivity. reflexivity. intros. destruct p0 as [p| p| ]; rename q into s. discriminate e1. discriminate e1. simpl in |- *. assert (Qhomographic_sign (a0 + c0) (b0 + d0) (e0 + g0) (f0 + h0) p3 (Qquadratic_signok_0 e0 f0 g0 h0 p3 H3) = Qhomographic_sign (a0 + c0) (b0 + d0) (e0 + g0) (f0 + h0) p3 s). apply Qhomographic_sign_equal. rewrite H. reflexivity. intros. simpl in |- *. rewrite H. reflexivity. intros. simpl in |- *. rewrite H. reflexivity. intros. simpl in |- *. rewrite H. reflexivity. intros. simpl in |- *. rewrite H. reflexivity. Qed.
imports: Coq(ZArithRing) QArithSternBrocot(Qhomographic_sign) QArithSternBrocot(Zaux)