isabelle/valid/algebra_sqineq_2at2pclta2c2p41pc.thy

(*
  Authors: Albert Qiaochu Jiang
*)

theory algebra_sqineq_2at2pclta2c2p41pc imports
  Complex_Main
begin

theorem algebra_sqineq_2at2pclta2c2p41pc:
  fixes a c :: real
  shows "2 * a * (2+c) \<le> a^2 + c^2 + 4 * (1+c)"
  sorry

end