Remove more TODOs

theories/examples/lock/proof_ticket_lock_gps.v

@@ -184,20 +184,11 @@ Proof.
       apply set_unfold_2. move => ? [[? [_ [? ?]]] _]. lia.
 Qed.
 
-(* TODO : move *)
-Lemma set_seq_size (s n: nat):  size (set_seq s n : gset nat) = n.
-Proof.
-  induction n as [|n IHn]; [done|].
-  rewrite set_seq_S_end_union_L /= size_union.
-  - rewrite IHn size_singleton. lia.
-  - apply disjoint_singleton_l.
-    move => /elem_of_set_seq [_ ?]. lia.
-Qed.
 Lemma Waiting_dom_size C M
   (DS : dom (gset nat) M ≡ set_seq 0 (Pos.to_nat C)):
   Z.pos C = size (dom (gset nat) M).
 Proof.
-  by rewrite (set_size_proper _ _ DS) -positive_nat_Z set_seq_size.
+  by rewrite (set_size_proper _ _ DS) -positive_nat_Z size_set_seq.
 Qed.
 
 Lemma Waiting_size_le C M n