proposition: Lemma Qquadratic_sign_sign_dec : 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), {q_sign a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero = 0%Z} + {q_sign a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero = 1%Z} + {q_sign a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero = (-1)%Z}.
proof: Proof. intros. unfold q_sign in |- *. generalize (Qquadratic_sign_sign a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero). case (Qquadratic_sign a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero). intros l1 L2. trivial. Qed.
imports: Coq(ZArithRing) QArithSternBrocot(Qhomographic_sign) QArithSternBrocot(Zaux)