refactor(Combinatorics/SimpleGraph/Copy): rename copy counts, introduce Sub subtype

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
new type `Sub G H` (subgraphs of `H` isomorphic to `G`) 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.
* Add `abbrev Sub G H := {H' : H.Subgraph // Nonempty (G ≃g H'.coe)}`;
  redefine `subCount` as `Fintype.card (G.Sub H)` (was the inline filter-set).
* Add `instance uniqueSubBot : Unique ((⊥ : SimpleGraph W).Sub H)` factoring
  the singleton-empty-subgraph fact out of `subCount_bot`.
* Drop `copyCount_eq_card_image_copyToSubgraph` (legacy filter-form bridge,
  unused after the type-form refactor).
* 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