proposition: Lemma Qquadratic_denom_nonzero_Zero_Zero_Zero_always : forall (h : Z) (s1 s2 : Q), h <> 0%Z -> Qquadratic_denom_nonzero 0 0 0 h s1 s2.
proof: Proof. intros h s1 s2 Hh. generalize h Hh s2. abstract (induction s1 as [| p| p]; intros; case s0; [ apply Qquadraticok00 | intro p; apply Qquadraticok01 with p | intro p; apply Qquadraticok02 with p | apply Qquadraticok10 with p | intro p0; apply Qquadraticok11 with p p0 | intro p0; apply Qquadraticok12 with p p0 | apply Qquadraticok20 with p | intro p0; apply Qquadraticok21 with p p0 | intro p0; apply Qquadraticok22 with p p0 ]; simpl in |- *; reflexivity || apply Qhomographic_sg_denom_nonzero_Zero_always || (try apply Qquadratic_sg_denom_nonzero_Zero_Zero_Zero_always); assumption). Defined.
imports: QArithSternBrocot(general_Q Zaux)