proposition: Lemma always_nonzero_Qhomographic_sg_denom_nonzero : forall (d : Z) (p : Qpositive), Qhomographic_sg_denom_nonzero 0 d p -> d <> 0%Z.
proof: Proof. intros. intro. apply (Qhomographic_sg_denom_nonzero_nonzero 0 d p); solve [ constructor | assumption ]. Defined.
imports: Coq(ZArithRing)