proposition: Lemma Qhomographic_sg_denom_nonzero_nonzero_2 : forall (c d : Z) (p : Qpositive), Qhomographic_sg_denom_nonzero c d p -> c <> d \/ c <> 0%Z.
proof: Proof. intros. apply double_not_equal_zero. intros (Hc, Hd). apply (Qhomographic_sg_denom_nonzero_nonzero c d p); assumption. Defined.
imports: Coq(ZArithRing)