proposition: Lemma Qquadratic_denom_nonzero_Zero_Zero_ONE_Zero : forall (s1 s2 : Q) (H_nonzero_s2 : s2 <> Zero :>Q), Qquadratic_denom_nonzero 0 0 1 0 s1 s2.
proof: Proof. intros. apply (Qquadratic_denom_nonzero_Zero_Zero_always_Zero 1 s1 s2 H_nonzero_s2). abstract discriminate. Defined.
imports: QArithSternBrocot(general_Q Zaux)