`No more subgoals, but there are non-instantiated existential variables` in Coq proof language?

I was following (incomplete) examples in Coq 8.5p1 's reference manual in chapter 11 about the mathematical/declarative proof language. In the example below for iterated equalities (~= and =~), I got a warning Insufficient Justification for rewriting 4 into 2+2, and eventually got an error saying:

No more subgoals, but there are non-instantiated existential variables:

?Goal : [x : R H : x = 2 _eq0 : 4 = x * x |- 2 + 2 = 4]

You can use Grab Existential Variables.

Example:

Goal forall x, x = 2 -> x + x = x * x.
Proof. 
proof. Show.
let x:R. 
assume H: (x = 2). Show. 
have ( 4 = 4). Show.
~= (2*2). Show. 
~= (x*x) by H. Show.
=~ (2+2). Show. (*Problem Here: Insufficient Justification*)
=~ H':(x + x) by H.
thus thesis by H'.
end proof.
Fail Qed.

I'm not familiar with the mathematical proof language in Coq and couldn't understand why this happens. Can someone help explain how to fix the error?

--EDIT-- @Vinz

I had these random imports before the example:

Require Import Reals.
Require Import Fourier.

Solution

Your proof would work for nat or Z, but it fails in case of R.

From the Coq Reference Manual (v8.5):

The purpose of a declarative proof language is to take the opposite approach where intermediate states are always given by the user, but the transitions of the system are automated as much as possible.

It looks like the automation fails for 4 = 2 + 2. I don't know what kind of automation uses the declarative proof engine, but, for instance, the auto tactic is not able to prove almost all simple equalities, like this one:

Open Scope R_scope.
Goal 2 + 2 = 4. auto. Fail Qed.

And as @ejgallego points out we can prove 2 * 2 = 4 using auto only by chance:

Open Scope R_scope.
Goal 2 * 2 = 4. auto. Qed.
(* `reflexivity.` would do here *)

However, the field tactic works like a charm. So one approach would be to suggest the declarative proof engine using the field tactic:

Require Import Coq.Reals.Reals.
Open Scope R_scope.
Unset Printing Notations.  (* to better understand what we prove *)
Goal forall x, x = 2 -> x + x = x * x.
Proof.
  proof.
  let x : R. 
  assume H: (x = 2).
  have (4 = 4).
  ~= (x*x) by H.
  =~ (2+2) using field.  (* we're using the `field` tactic here *)
  =~ H':(x + x) by H.
  thus thesis by H'.
  end proof.
Qed.