proposition: Lemma Qhomographic_denom_nonzero_0 : forall c d : Z, Qhomographic_denom_nonzero c d Zero -> d <> 0%Z.
proof: Proof. intros; abstract (inversion_clear H; assumption || discriminate H0). Defined.
imports: Coq(ZArithRing)