Use of contradiction tactic

Using Rocq
5

For future people who might find it helpful, here is how I solved it, it was not the theorem, just a trick in the proof to get the contradiction.

Theorem test : exists n : nat, (P n -> forall m : nat, P m).
Proof.
  destruct Hypn as [n T].
  assert (Hn : (forall z : nat, P z) \/ ~((forall z : nat, P z))).
  { apply Helper. }
  destruct Hn as [H1 | H2].
  - exists n.
    intros _.
    exact H1.
  - assert (Hz : exists z, ~P z).
  {
    apply not_all_ex_not. 
    exact H2.
  }
  destruct Hz as [z H_not_z].
  exists z.
  intros Hz.
  contradiction.
  Qed.

Thanks for the help!