How to deal with lemma only used once in Coq?

Question

I've declared a lemma that I used only for one proof (SoS2_imp_Pos in the code). Is it problematic? How can I do otherwise? I thought about using assert forall s t u, SoS2 u s t -> PoS s u, but I'm not sure it is a better choice.

Lemma SoS2_imp_Pos: forall s t u, SoS2 u s t -> PoS s u.
Proof.
  intros s t u H; apply NNPP; intros NPoSsu.
  pose proof (slot_strong_supp u s NPoSsu) as (v & PoSvs & NOoSvu).
  apply pos_implies_overlap in PoSvs.
  destruct H with (v:=v).
  destruct H1.
  left; apply oos_comm; assumption.
  apply NOoSvu.
  exists x; apply and_comm; assumption.
Qed.

Theorem SoS_equiv_SoS2: forall u s t, SoS u s t <-> SoS2 u s t.
Proof.
  intros u s t.
  split.
  - intros (PoSsu & PoStu & H) v.
    split.
    + intros (w & PoSwu & PoSwv).
      pose proof (H w PoSwu) as [H1|H1];
      [left|right];
      apply part_overlap_implies_whole_overlap with (t:=w);
      assumption.
    + intros [|];
      apply oos_comm in H0;
      apply oos_comm;
      [apply part_overlap_implies_whole_overlap with (t:=s)|
       apply part_overlap_implies_whole_overlap with (t:=t)];
      assumption.
  - intros H.
    repeat split.
    + apply SoS2_imp_Pos with (t:=t); assumption.
    + apply SoS2_imp_Pos with (t:=s).
      unfold SoS2 in *.
      setoid_rewrite (or_comm (OoS s _)) in H.
      assumption.
    + intros v PoSvu.
      apply H.
      apply oos_comm.
      apply pos_implies_overlap.
      assumption.
Qed.

Answer 1

No, I think it's OK. If you want to underline it's just a step of the proof, you can downgrade it to Remark.