proposition: Lemma Qhomographic_denom_nonzero_1 : forall (c d : Z) (p : Qpositive), Qhomographic_denom_nonzero c d (Qpos p) -> Qhomographic_sg_denom_nonzero c d p.
proof: Proof. intros; abstract (inversion_clear H; solve [ assumption | match goal with | id1:(?X1 = ?X2) |- ?X3 => try discriminate id1; clear id1 end | match goal with | id1:(?X1 = ?X2) |- ?X3 => injection id1; intro H_injected; rewrite H_injected; assumption end ]). Defined.
imports: Coq(ZArithRing)