proposition: Lemma Qhomographic_denom_nonzero_always_Zero : forall (c : Z) (s : Q) (H_nonzero_s : s <> Zero :>Q), c <> 0%Z -> Qhomographic_denom_nonzero c 0 s.
proof: Proof. abstract (intros; destruct s as [| p| p]; [ Falsum | apply Qhomographicok1 with p | apply Qhomographicok2 with p ]; try reflexivity; apply Qhomographic_sg_denom_nonzero_always_Zero; try match goal with | id1:?X2 |- ((- ?X1)%Z <> 0%Z) => apply Zopp_app end; assumption). Defined.
imports: Coq(ZArithRing)