proposition: Lemma Qquadratic_sign_nRdL_One : forall (a b c d e f g h : Z) (p1 p2 : Qpositive) (H_Qquadratic_sg_denom_nonzero : Qquadratic_sg_denom_nonzero e f g h p1 p2) (l1 na nb nc nd : Z) (l3 : Qpositive) (H_Qhomographic_sg_denom_nonzero : Qhomographic_sg_denom_nonzero (e + f) (g + h) p1), (l1, (na, (nb, (nc, nd)), l3)) = Qhomographic_sign (a + b) (c + d) (e + f) (g + h) p1 H_Qhomographic_sg_denom_nonzero -> p1 <> One -> p2 = One -> Qquadratic_sign a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero = (l1, (0%Z, (na, (0%Z, nb)), (0%Z, (nc, (0%Z, nd))), (l3, One))).
proof: Proof. intros. destruct p2 as [q| q| ]; repeat (apply False_ind; discriminate H1). destruct p1 as [p| p| ]. unfold Qquadratic_sign in |- *. rewrite Qhomographic_sign_equal with (H1 := Qquadratic_signok_0' e f g h (nR p) H_Qquadratic_sg_denom_nonzero) (H2 := H_Qhomographic_sg_denom_nonzero). rewrite <- H. reflexivity. unfold Qquadratic_sign in |- *. rewrite Qhomographic_sign_equal with (H1 := Qquadratic_signok_0' e f g h (dL p) H_Qquadratic_sg_denom_nonzero) (H2 := H_Qhomographic_sg_denom_nonzero). rewrite <- H. reflexivity. Falsum. Qed.
imports: Coq(ZArithRing) QArithSternBrocot(Qhomographic_sign) QArithSternBrocot(Zaux)