proposition: Lemma Qquadratic_11 : forall (e f g h : Z) (p1 p2 : Qpositive), Qquadratic_denom_nonzero e f g h (Qpos p1) (Qpos p2) -> Qquadratic_sg_denom_nonzero e f g h p1 p2.
proof: Proof. intros. abstract (inversion H; try solve [ assumption | repeat match goal with | id1:(?X1 = ?X2) |- ?X3 => try discriminate id1; clear id1 end ]; repeat match goal with | id1:(?X1 ?X2 = ?X1 ?X3) |- ?X4 => let tt := eval compute in (f_equal Q_tail id1) in rewrite tt end; assumption). Defined.
imports: QArithSternBrocot(general_Q Zaux)