proposition: Lemma Qhomographic_signok_2 : forall (c d : Z) (xs : Qpositive), Qhomographic_sg_denom_nonzero c d (nR xs) -> Qhomographic_sg_denom_nonzero c (c + d) xs.
proof: Proof. intros. inversion H. discriminate H0. assumption. Defined.
imports: Coq(ZArithRing)