proposition: Lemma Qhomographic_sign_nR_4 : forall (a b c d : Z) (p xs : Qpositive) (H_Qhomographic_sg_denom_nonzero : Qhomographic_sg_denom_nonzero c (c + d) xs) (H_Qhomographic_sg_denom_nonzero_nR : Qhomographic_sg_denom_nonzero c d (nR xs)), b = 0%Z -> d <> 0%Z -> ~ (0 < outside_interval c d)%Z -> ~ (outside_interval c d < 0)%Z -> Qhomographic_sign a b c d (nR xs) H_Qhomographic_sg_denom_nonzero_nR = Qhomographic_sign a (a + b) c (c + d) xs H_Qhomographic_sg_denom_nonzero.
proof: Proof. intros; 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; [ Falsum | case (Z_lt_dec (outside_interval c d) 0); intro Ho2'; [ Falsum | apply Qhomographic_sign_equal ] ] ] | Falsum ]. Defined.
imports: Coq(ZArithRing)