proposition: Lemma Qhomographic_sign_nR_2 : forall (a b c d : Z) (p xs : Qpositive) (H_Qhomographic_sg_denom_nonzero : Qhomographic_sg_denom_nonzero c d p), p = nR xs -> b = 0%Z -> d <> 0%Z -> (0 < outside_interval c d)%Z -> Qhomographic_sign a b c d p H_Qhomographic_sg_denom_nonzero = (Z.sgn a, (a, (b, (c, d)), p)).
proof: Proof. intros; generalize H_Qhomographic_sg_denom_nonzero; clear H_Qhomographic_sg_denom_nonzero; rewrite H; intros H_Qhomographic_sg_denom_nonzero; simpl in |- *; case (Z_zerop b); intro Hb; [ case (Z_zerop d); intro Hd; [ Falsum | case (Z_lt_dec 0 (outside_interval c d)); intro Ho2; [ reflexivity | Falsum ] ] | Falsum ]. Defined.
imports: Coq(ZArithRing)