proposition: Lemma sg_sign_dec : 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 = 0%Z} + {h_sign a b c d p H_Qhomographic_sg_denom_nonzero = 1%Z} + {h_sign a b c d p H_Qhomographic_sg_denom_nonzero = (-1)%Z}.
proof: Proof. intros. unfold h_sign in |- *. generalize (sg_sign a b c d p H_Qhomographic_sg_denom_nonzero). case (Qhomographic_sign a b c d p H_Qhomographic_sg_denom_nonzero). intros l1 L2. trivial. Defined.
imports: Coq(ZArithRing)