proposition: Lemma sg_One_2 : forall (a b c d : Z) (p : Qpositive) (H_Qhomographic_sg_denom_nonzero : Qhomographic_sg_denom_nonzero c d p), p = One -> Z.sgn (a + b) = 0%Z -> Qhomographic_sign a b c d p H_Qhomographic_sg_denom_nonzero = (0%Z, (a, (b, (c, d)), One)).
proof: Proof. intros. destruct p as [q| q| ]; repeat (apply False_ind; discriminate H). simpl in |- *. case (Z.eq_dec (Z.sgn (a + b)) 0). intro. reflexivity. intro. Falsum. Defined.
imports: Coq(ZArithRing)