proposition: Lemma Qhomographic_sg_denom_nonzero_nonzero_3 : forall (c d : Z) (p : Qpositive), Qhomographic_sg_denom_nonzero c d p -> c <> 0%Z \/ d <> 0%Z.
proof: Proof. intros c d p H_Qhomographic_sg_denom_nonzero. generalize (Qhomographic_sg_denom_nonzero_nonzero_2 c d p H_Qhomographic_sg_denom_nonzero); intros [Hcd| Hd]; [ case (Z_zerop c); intro Hc; [ right; apply sym_not_equal; rewrite Hc in Hcd | left ] | left ]; try assumption. Defined.
imports: Coq(ZArithRing)