proposition: Lemma Qquadratic_sg_denom_nonzero_nonzero : forall (e f g h : Z) (p1 p2 : Qpositive), e = 0%Z -> f = 0%Z -> g = 0%Z -> h = 0%Z -> ~ Qquadratic_sg_denom_nonzero e f g h p1 p2.
proof: Proof. intros e f g h p1 p2 He Hf Hg Hh H_Qquadratic_sg_denom_nonzero. generalize He Hf Hg Hh. elim H_Qquadratic_sg_denom_nonzero; intros; first [ refine (Qhomographic_sg_denom_nonzero_nonzero (e0 + f0) (g0 + h0) p0 _ _ H0) | refine (Qhomographic_sg_denom_nonzero_nonzero (e0 + g0) (f0 + h0) p3 _ _ H0) | apply H0 ]; repeat match goal with | id1:(?X1 = ?X2) |- ?X3 => rewrite id1 end; constructor. Defined.
imports: QArithSternBrocot(general_Q Zaux)