UIP on Nat in Coq

CoqNatUIP.v

Definition lemma {n m : nat} (p : n = m) : pred n = pred m := f_equal pred p.
Definition lemma2 {n m : nat} (p : n = m) : S n = S m := f_equal S p.
Definition lemma3 {n m : nat} (p : S n = S m) : lemma2 (lemma p) = p
  := match p with | eq_refl => eq_refl end.

(* Definition bruh {n} (a : nat) (p : S n = a) : Prop.
Proof.
  destruct a.
  - exact True.
  - exact (@lemma2 n a (@lemma (S n) (S a) p) = p).
Defined.

Definition lemma3 {n m : nat} (p : S n = S m) : lemma2 (lemma p) = p.
Proof.
  simpl.
  apply eq_ind_dep with (e := p) (P := bruh).
  simpl. trivial.
Qed. *)

Definition lemma5 {n : nat} (p : S n = S n) :
  lemma2 (lemma p) = lemma2 eq_refl -> p = eq_refl.
Proof.
  rewrite lemma3.
  compute.
  trivial.
Qed.

Definition test (n : nat) (p : n = n) : p = eq_refl.
Proof.
  induction n.
  exact (match p with | eq_refl => eq_refl end).
  pose proof (fun pp : S n = S n => IHn (lemma pp)) as q.
  pose proof (f_equal lemma2 (q p)) as q1.
  apply lemma5.
  trivial.
Qed.

Thanks to @PhotonQuantum for some help & motivating this