proposition: Theorem quadratic_algorithm_is_correct : forall (a b c d e f g h : Z) (q1 q2 : Q) (H_denom : Qplus (Qplus (Qplus (Qmult (Qmult e q1) q2) (Qmult f q1)) (Qmult g q2)) h <> Zero), Qquadratic a b c d e f g h q1 q2 (Qquadratic_denom_nonzero_correct_2 e f g h q1 q2 H_denom) = 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)).
proof: Proof. intros a b c d e f g h q1 q2 H_denom; apply (quadratic a b c d e f g h q1 q2 (Qquadratic_denom_nonzero_correct_2 e f g h q1 q2 H_denom)). Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)