refactor(Combinatorics/SimpleGraph/Copy): rename copy counts and unify graph variables

Aligns the labelled/unlabelled naming in `Copy.lean` so that the type `Copy G H`
(labelled, injective hom from `G` into `H`) is paired with the count
`H.copyCount G` (labelled count, host-first per mathlib op convention) and the
`Sub G H` carrier (introduced in the previous PR) is paired with the count
`H.subCount G`. Also unifies the graph-variable letters: the `A B C` set
that was local to `Copy.lean` is dropped in favour of mathlib's wider `G H I`
convention, with `α β γ` → `V W X` correspondingly. Within the new convention
`G` is the guest (pattern, contained side) and `H` is the host (container),
matching `G ⊑ H` and the hom direction `G →g H`.

Types are pattern-first (`Copy G H`, `Sub G H`); operations are host-first via
dot notation (`H.copyCount G`, `H.subCount G`, `H.killCopies G`). This matches
the existing mathlib convention split (hom types use source-first, host-side
operations use the host as the dot-notation receiver).

Changes:

* Rename `labelledCopyCount → copyCount` (with British `@[deprecated]` alias
  `labelledCopyCount`). The previous `copyCount → subCount` rename has no
  alias — `copyCount` is reassigned to mean the labelled count. Same for the
  `_of_isEmpty` / `_eq_zero` / `_pos` lemma families.
* Rename `copyCount_bot → subCount_emptyGraph` and `uniqueSubBot →
  uniqueSubEmptyGraph` (folding the planned `_bot → _emptyGraph` naming
  alignment with #23838's convention; both names were introduced in the
  preceding `feat/copy-sub-abbrev` PR and would otherwise have needed a
  separate rename PR with brief-window deprecated aliases).
* Unify `A B C / α β γ` to `G H I / V W X` throughout. Variable block follows
  the mathlib convention (cf. `SimpleGraph/Maps.lean`): subscripted names
  (`G₁ G₂ G₃`) for same-vertex-type variants used in `≤` chains and `ofLE`;
  primed names (`G'`, `H'`) on independent universes (`V'`, `W'`) for the
  cross-universe variants used in `isContained_congr` / `free_congr` (and
  their `_left` / `_right` partial-iso forms). This preserves the universe
  polymorphism the old `A B C / α β γ` block provided implicitly and that
  `Extremal/Basic.lean` (line 96, `← free_congr .refl (.map e G)`) relies
  on.
* Fix the docstring direction on `IsContained.trans` and `.trans'`: the
  previous wording ("`G` contains `H`") read the relation backwards relative
  to the lemma signature (`G ⊑ H` means `G` is contained in `H`).
* Update module docstring (`Sub`/`subCount` bullets, logical-flow ordering,
  `SimpleGraph.Subgraph` cross-references); add TODOs for `homCount` and
  the three densities.

Author: FordUniver