proposition: Lemma Qquadratic_sg_denom_nonzero_nonzero_3 : forall (g h : Z) (p1 p2 : Qpositive), Qquadratic_sg_denom_nonzero 0 0 g h p1 p2 -> g <> 0%Z \/ h <> 0%Z.
proof: Proof. intros. case (Z_zerop g); [ intro; case (Z_zerop h); [ intro; idtac | intro; right ] | intro; left ]; try assumption. apply False_ind. apply (Qquadratic_sg_denom_nonzero_nonzero 0 0 g h p1 p2); try solve [ constructor | assumption ]. Defined.
imports: QArithSternBrocot(general_Q Zaux)