proposition: Lemma Qquadratic_sign_nRdL_nRdL_1 : 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), p1 <> One -> p2 <> One -> b = 0%Z /\ c = 0%Z /\ d = 0%Z -> f = 0%Z /\ g = 0%Z /\ h = 0%Z -> Qquadratic_sign a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero = ((Z.sgn a * Z.sgn e)%Z, (a, (b, (c, d)), (e, (f, (g, h))), (p1, p2))).
proof: Proof. intros. destruct p1 as [q| q| ]; solve [ Falsum ] || let T_local := (simpl in |- *; case (three_integers_dec_inf b c d); [ intro; case (three_integers_dec_inf f g h); [ intro; reflexivity | intro H3; Falsum ] | intro H3; Falsum ]) in (destruct p2 as [q0| q0| ]; [ T_local | T_local | Falsum ]). Qed.
imports: Coq(ZArithRing) QArithSternBrocot(Qhomographic_sign) QArithSternBrocot(Zaux)