proposition: Lemma Qhomographic_sg_denom_nonzero_nonzero : forall (c d : Z) (p : Qpositive), c = 0%Z -> d = 0%Z -> ~ Qhomographic_sg_denom_nonzero c d p.
proof: Proof. intros c d p Hc Hd H_Qhomographic_sg_denom_nonzero. generalize Hc Hd. elim H_Qhomographic_sg_denom_nonzero; intros; apply H0; first [ assumption | rewrite Hc0; rewrite Hd0; constructor ]. Defined.
imports: Coq(ZArithRing)