isabelle/valid/algebra_binomnegdiscrineq_10alt28asqp1.thy

(*
  Authors: Albert Qiaochu Jiang
*)

theory algebra_binomnegdiscrineq_10alt28asqp1 imports
  Complex_Main
begin

theorem algebra_binomnegdiscrineq_10alt28asqp1:
  fixes a :: real
  shows "10 * a \<le> 28 * a^2 + 1"
  sorry

end