proposition: Lemma Qquadratic_denom_nonzero_Zero_Zero_Zero_ONE : forall s1 s2 : Q, Qquadratic_denom_nonzero 0 0 0 1 s1 s2.
proof: Proof. intros. apply Qquadratic_denom_nonzero_Zero_Zero_Zero_always. abstract discriminate. Defined.
imports: QArithSternBrocot(general_Q Zaux)