(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Definition: quadratic_root_plus                                            *)
(* Chapter: LEG                                                               *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-02-07                                                           *)
(* ========================================================================== *)




(*
Lemmas Elementary Geometry  (def:calE), RPFVZDI
*)


(* deprecated. Moved to sphere.hl *)

module type Quadratic_root_plus_def_type = sig
  val quadratic_root_plus : thm
end;;



module Quadratic_root_plus : Quadratic_root_plus_def_type = struct

 let quadratic_root_plus = 
   new_definition `quadratic_root_plus (a, b, c) = ( -- b + sqrt(b pow 2 - &4 * a * c))/ (&2 * a)`;;

end;;