proposition: Lemma Qquadratic_denom_nonzero_Zero_Zero_always_Zero : forall (g : Z) (s1 s2 : Q) (H_nonzero_s2 : s2 <> Zero :>Q), g <> 0%Z -> Qquadratic_denom_nonzero 0 0 g 0 s1 s2.
proof: Proof. intros g s1 s2 H_nonzero_s2 Hg. generalize g Hg s2 H_nonzero_s2. abstract (induction s1 as [| p| p]; intros; destruct s0 as [| p0| p0]; [ Falsum | apply Qquadraticok01 with p0 | apply Qquadraticok02 with p0 | Falsum | apply Qquadraticok11 with p p0 | apply Qquadraticok12 with p p0 | Falsum | apply Qquadraticok21 with p p0 | apply Qquadraticok22 with p p0 ]; simpl in |- *; reflexivity || apply Qhomographic_sg_denom_nonzero_always_Zero || (try apply Qquadratic_sg_denom_nonzero_Zero_Zero_always_Zero); try match goal with | id1:?X2 |- ((- ?X1)%Z <> 0%Z) => apply Zopp_app end; assumption). Defined.
imports: QArithSternBrocot(general_Q Zaux)