fact: Definition spec_q (a b c d e f g h : Z) (q1 q2 : Q) : Q := Qmult (Qplus (Qplus (Qplus (Qmult (Qmult a q1) q2) (Qmult b q1)) (Qmult c q2)) d) (Qinv (Qplus (Qplus (Qplus (Qmult (Qmult e q1) q2) (Qmult f q1)) (Qmult g q2)) h)).
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)