proposition: Lemma Qquadratic_sg_denom_nonzero_nonzero_inf : forall (e f g h : Z) (p1 p2 : Qpositive), Qquadratic_sg_denom_nonzero e f g h p1 p2 -> {e <> 0%Z} + {f <> 0%Z} + {g <> 0%Z} + {h <> 0%Z}.
proof: Proof. intros e f g h p1 p2 H_Qquadratic_sg_denom_nonzero. case (Z_zerop e); [ case (Z_zerop f); [ case (Z_zerop g); [ case (Z_zerop h); [ intros; apply False_rec; apply (Qquadratic_sg_denom_nonzero_nonzero_1 e f g h p1 p2 H_Qquadratic_sg_denom_nonzero); repeat split; assumption | intros ] | intros ] | intros ] | intros ]; [ right | left; right | left; left; right | left; left; left ]; assumption. Defined.
imports: QArithSternBrocot(general_Q Zaux)