proposition: Lemma Qhomographic_sign_equal : forall (a b c d : Z) (p : Qpositive) (H1 H2 : Qhomographic_sg_denom_nonzero c d p), Qhomographic_sign a b c d p H1 = Qhomographic_sign a b c d p H2.
proof: Proof. intros. generalize H2 H1 a b. intro. abstract let T_local := (intros; simpl in |- *; rewrite H; reflexivity) in (elim H0 using Qhomographic_sg_denom_nonzero_inv_dep; intros; [ destruct p0 as [q| q| ]; [ discriminate e | discriminate e | simpl in |- *; case (Z.eq_dec (Z.sgn (a0 + b0)) 0); case (Z.eq_dec (Z.sgn (a0 + b0)) (Z.sgn (c0 + d0))); intros; reflexivity ] | T_local | T_local ]). Defined.
imports: Coq(ZArithRing)