proposition: Lemma Qhomographic_denom_nonzero_Zero_always : forall (d : Z) (s : Q), d <> 0%Z -> Qhomographic_denom_nonzero 0 d s.
proof: Proof. abstract (intros; destruct s as [| p| p]; [ apply Qhomographicok0 | apply Qhomographicok1 with p | apply Qhomographicok2 with p ]; reflexivity || (try apply Qhomographic_sg_denom_nonzero_Zero_always); assumption). Defined.
imports: Coq(ZArithRing)