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
`UnlabeledCopy G H` carrier (introduced in the previous PR) is paired with the
count `H.unlabeledCopyCount 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 guest-first (`Copy G H`, `UnlabeledCopy G H`); operations are
host-first via dot notation (`H.copyCount G`, `H.unlabeledCopyCount 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 → unlabeledCopyCount` 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 → unlabeledCopyCount_bot` (count name rename only;
  `_bot` spelling preserved per @SnirBroshi).
* 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 (`UnlabeledCopy` / `unlabeledCopyCount` bullets,
  logical-flow ordering, `SimpleGraph.Subgraph` cross-references); add TODOs
  for `homCount` and the three densities.

Author: FordUniver