proposition: Lemma Qhomographic_denom_nonzero_ONE_Zero : forall (s : Q) (H_nonzero_s : s <> Zero :>Q), Qhomographic_denom_nonzero 1 0 s.
proof: Proof. intros; apply Qhomographic_denom_nonzero_always_Zero; assumption || (abstract discriminate). Defined.
imports: Coq(ZArithRing)