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. The few four-graph
  statements (`isContained_congr`, `free_congr`) take explicit
  `{V₂ W₂ : Type*}` (and `_right` variants take `{W₂ : Type*}`) so that the
  host/guest vertex types remain independent across the iso — restoring the
  universe polymorphism the old `α β γ δ` variable block provided implicitly,
  which `Extremal/Basic.lean` relies on at the call site
  `← free_congr .refl (.map e G)`.
* 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