proposition: Lemma Qhomographic_sg_denom_nonzero_always_Zero : forall (c : Z) (p : Qpositive), c <> 0%Z -> Qhomographic_sg_denom_nonzero c 0 p.
proof: Proof. intros. induction p. apply Qhomographic_signok1. rewrite Zplus_0_r. replace c with (1 * c)%Z. apply Qhomographic_sg_denom_nonzero_always_1. assumption. constructor. constructor. rewrite Zmult_1_l. reflexivity. apply Qhomographic_signok2. rewrite Zplus_0_r. assumption. apply Qhomographic_signok0. reflexivity. rewrite Zplus_0_r. assumption. Defined.
imports: Coq(ZArithRing)