proposition: Lemma Qquadratic_sg_denom_nonzero_nonzero_1 : 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 (He, (Hf, (Hg, Hh))). exact (Qquadratic_sg_denom_nonzero_nonzero e f g h p1 p2 He Hf Hg Hh H_Qquadratic_sg_denom_nonzero). Defined.
imports: QArithSternBrocot(general_Q Zaux)