proposition: Lemma Qquadratic_10 : forall (e f g h : Z) (p1 : Qpositive), Qquadratic_denom_nonzero e f g h (Qpos p1) Zero -> Qhomographic_sg_denom_nonzero f h p1.
proof: Proof. intros. abstract (inversion H; try solve [ assumption | repeat match goal with | id1:(?X1 = ?X2) |- ?X3 => try discriminate id1; clear id1 end ]; generalize (f_equal Q_tail H0); simpl in |- *; intro H_p; rewrite H_p; assumption). Defined.
imports: QArithSternBrocot(general_Q Zaux)