(*
  Authors: Albert Qiaochu Jiang
*)

theory algebra_amgm_faxinrrp2msqrt2geq2mxm1div2x imports
  Complex_Main
begin

theorem algebra_amgm_faxinrrp2msqrt2geq2mxm1div2x:
  "\<And>x. (x>0) \<Longrightarrow> 2 - sqrt 2 \<ge> 2 - x - 1/ (2 * x)"
  sorry

end