isabelle/valid/algebra_manipexpr_2erprsqpesqeqnrpnesq.thy

(*
  Authors: Albert Qiaochu Jiang
*)

theory algebra_manipexpr_2erprsqpesqeqnrpnesq imports
Complex_Main

begin

theorem algebra_manipexpr_2erprsqpesqeqnrpnesq:
  fixes e r :: complex
  shows "2 * (e * r) + (e^2 + r^2) = (-r + (-e))^2"
  sorry


end