proposition: Lemma quadraticAcc_positive_numerator : forall (a b c d e f g h : Z) (p1 p2 : Qpositive), quadraticAcc a b c d e f g h p1 p2 -> Qlt Zero (Qplus (Qplus (Qplus (Qmult (Qmult a (Qpos p1)) (Qpos p2)) (Qmult b (Qpos p1))) (Qmult c (Qpos p2))) d).
proof: Proof. intros; elim (quadraticAcc_positive _ _ _ _ _ _ _ _ _ _ H); trivial. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)