You seem to be confusing

forall n0 : nat,
(Nat.even n0 = true -> exists z : nat, n0 = z * 2)
->
forall n : nat,
Nat.even n = true -> exists z : nat, n = z * 2

with

(forall n0 : nat,
(Nat.even n0 = true -> exists z : nat, n0 = z * 2))
->
forall n : nat,
Nat.even n = true -> exists z : nat, n = z * 2

The second proof is indeed trivial:

Goal (forall n0 : nat,
     (Nat.even n0 = true -> exists z : nat, n0 = z * 2)) ->
forall n : nat, Nat.even n = true -> exists z : nat, n = z * 2.
Proof.
  trivial.
Qed.

whereas the first proof is not. Note carefully the extra pair of parentheses in the second.

Here is an explicit example where you provably cannot distribute the forall quantification over implication:

Goal ~ forall n : nat, n <> 1 -> (forall n : nat, n <> 1).
Proof.
  intros H.
  now contradiction (H _ (n_Sn 0) 1).
Qed.

Contrast with

Goal (forall n : nat, n <> 1) -> (forall n : nat, n <> 1).
Proof.
  intros H.
  assumption.
Qed.

You seem to be confusing

forall n0 : nat,
(Nat.even n0 = true -> exists z : nat, n0 = z * 2)
->
forall n : nat,
Nat.even n = true -> exists z : nat, n = z * 2

with

(forall n0 : nat,
(Nat.even n0 = true -> exists z : nat, n0 = z * 2))
->
forall n : nat,
Nat.even n = true -> exists z : nat, n = z * 2

The second proof is indeed trivial:

Goal (forall n0 : nat,
     (Nat.even n0 = true -> exists z : nat, n0 = z * 2)) ->
forall n : nat, Nat.even n = true -> exists z : nat, n = z * 2.
Proof.
  trivial.
Qed.

whereas the first proof is not. Note carefully the extra pair of parentheses in the second.

Here is an explicit example where you provably cannot distribute the forall quantification over implication:

Goal ~ forall n : nat, n <> 1 -> (forall n : nat, n <> 1).
Proof.
  intros H.
  now contradiction (H _ (n_Sn 0) 1).
Qed.

Contrast with

Goal (forall n : nat, n <> 1) -> (forall n : nat, n <> 1).
Proof.
  intro.
  assumption.
Qed.

You seem to be confusing

forall n0 : nat,
(Nat.even n0 = true -> exists z : nat, n0 = z * 2)
->
forall n : nat,
Nat.even n = true -> exists z : nat, n = z * 2

with

(forall n0 : nat,
(Nat.even n0 = true -> exists z : nat, n0 = z * 2))
->
forall n : nat,
Nat.even n = true -> exists z : nat, n = z * 2

The second proof is indeed trivial:

Goal (forall n0 : nat,
     (Nat.even n0 = true -> exists z : nat, n0 = z * 2)) ->
forall n : nat, Nat.even n = true -> exists z : nat, n = z * 2.
Proof.
  trivial.
Qed.

whereas the first proof is not. Note carefully the extra pair of parentheses in the second.

Here is an explicit example where you provably cannot distribute the forall quantification over implication:

Goal ~ (forall n : nat, n <> 1 -> (forall n : nat, n <> 1)).
Proof.
  intros H.
  assert (0 <> 1) as H0 by auto.
  pose proof (H _ H0 1).
  contradiction.
Qed.

You seem to be confusing

forall n0 : nat,
(Nat.even n0 = true -> exists z : nat, n0 = z * 2)
->
forall n : nat,
Nat.even n = true -> exists z : nat, n = z * 2

with

(forall n0 : nat,
(Nat.even n0 = true -> exists z : nat, n0 = z * 2))
->
forall n : nat,
Nat.even n = true -> exists z : nat, n = z * 2

The second proof is indeed trivial:

Goal (forall n0 : nat,
     (Nat.even n0 = true -> exists z : nat, n0 = z * 2)) ->
forall n : nat, Nat.even n = true -> exists z : nat, n = z * 2.
Proof.
  trivial.
Qed.

whereas the first proof is not. Note carefully the extra pair of parentheses in the second.

Here is an explicit example where you provably cannot distribute the forall quantification over implication:

Goal ~ forall n : nat, n <> 1 -> (forall n : nat, n <> 1).
Proof.
  intros H.
  now contradiction (H _ (n_Sn 0) 1).
Qed.

Contrast with

Goal (forall n : nat, n <> 1) -> (forall n : nat, n <> 1).
Proof.
  intros H.
  assumption.
Qed.