Grace/Cumulus/GraphTheory/TreePacking/Sequences.g17

Open in Workbench Download source

Imports

Decompositions · Nat.Least · Combinatorics.InclusionExclusion

Declarations

Source

1-- Kaiser's proof of the tree-packing theorem begins with the partition2-- sequence of a decomposition: starting from the trivial partition, each3-- step refines the current partition by the components of the first colour4-- disconnected inside a class, and the sequence grows strictly until it5-- stabilises at a partition on which every colour is internally connected.6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.GraphTheory.TreePacking.Sequences12import Decompositions13import Nat.Least14import Combinatorics.InclusionExclusion1516-- The class of a colour is a set of edges.17theorem Decomposition.class_subset (E T i : Set, k : Nat)18  requires decomposition : Decomposition(E, T, k)19  requires colour : i ∈ k20  shows T(i) ⊆ E21proof22  exact powerset.membership_iff.forward with23    (FunctionBetween.apply_closed with decomposition.left, colour)2425-- The class of a colour has its ends in V.26theorem Decomposition.ends (V E leftEnd rightEnd T i : Set, k : Nat)27  requires graph : Graph(V, E, leftEnd, rightEnd)28  requires decomposition : Decomposition(E, T, k)29  requires colour : i ∈ k30  shows ∀ e ∈ T(i), leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V31proof32  exact ends_in.subset with (Graph.ends with graph),33    (Decomposition.class_subset with decomposition, colour)3435-- The least colour whose class is not internally connected on P, or k when36-- every colour is: the colour c_i of the proof.37def disconnectedColour (leftEnd rightEnd T P : Set, k : Nat) : Set :=38  { i ∈ k | ¬InternallyConnected(leftEnd, rightEnd, T(i), P) }3940theorem disconnectedColour.subset (leftEnd rightEnd T P : Set, k : Nat)41  shows disconnectedColour(leftEnd, rightEnd, T, P, k) ⊆ ℕ42proof43  intros i member44  have natural := natural.member at k with i, member.left45  exact nat.omega.forward with natural4647-- When some colour is disconnected, the least one is a colour below k that48-- is not internally connected.49theorem disconnectedColour.least (leftEnd rightEnd T P : Set, k : Nat)50  requires some : disconnectedColour(leftEnd, rightEnd, T, P, k) ≠ ∅51  shows leastNatural(disconnectedColour(leftEnd, rightEnd, T, P, k)) ∈ k ∧52    ¬InternallyConnected(leftEnd, rightEnd,53      T(leastNatural(disconnectedColour(leftEnd, rightEnd, T, P, k))), P)54proof55  have inhabited := Nonempty.of_ne_empty with some56  exact leastNatural.member with inhabited, disconnectedColour.subset5758-- With no disconnected colour every colour is internally connected.59theorem disconnectedColour.empty_iff (leftEnd rightEnd T P : Set, k : Nat)60  shows disconnectedColour(leftEnd, rightEnd, T, P, k) = ∅ ↔61    (∀ i ∈ k, InternallyConnected(leftEnd, rightEnd, T(i), P))62proof63  constructor64  . intros none i colour65    by_contra disconnected66    have member : i ∈ disconnectedColour(leftEnd, rightEnd, T, P, k) :=67      ⟨colour, disconnected⟩68    rw none at member69    simp at member70  . intro internal71    ext i72    constructor73    . intro member74      exfalso75      exact member.right with (internal with i, member.left)76    . intro member77      simp [union2.membership, singleton.membership] at member7879-- The partition sequence P_0 = {V}, P_{n+1} = P_n refined by the least80-- disconnected colour, fixed once every colour is internally connected.81def partitionStep (V leftEnd rightEnd T P : Set, k : Nat) : Set :=82  { X ∈ 𝒫(V) |83    (disconnectedColour(leftEnd, rightEnd, T, P, k) = ∅ ∧ X ∈ P) ∨84    (disconnectedColour(leftEnd, rightEnd, T, P, k) ≠ ∅ ∧85      X ∈ refineBy(leftEnd, rightEnd,86        T(leastNatural(disconnectedColour(leftEnd, rightEnd, T, P, k))), P)) }8788def partitionSequence (V leftEnd rightEnd T : Set, k n : Nat) → Set89  | V, leftEnd, rightEnd, T, k, zero => {V}90  | V, leftEnd, rightEnd, T, k, succ(m) =>91    partitionStep(V, leftEnd, rightEnd, T,92      partitionSequence(V, leftEnd, rightEnd, T, k, m), k)9394-- The step keeps P when every colour is internally connected, and95-- otherwise refines it along the least disconnected colour.96theorem partitionStep.fixed (V leftEnd rightEnd T P : Set, k : Nat)97  requires partition : Partition(V, P)98  requires none : disconnectedColour(leftEnd, rightEnd, T, P, k) = ∅99  shows partitionStep(V, leftEnd, rightEnd, T, P, k) = P100proof101  ext X102  constructor103  . intro member104    obtain ⟨_, fixed | refined⟩ := member105    . exact fixed.right106    . exfalso107      exact refined.left with none108  . intro class109    have subset := (partition.left with X, class).left110    refine ⟨(powerset.membership_iff.backward with subset), _⟩111    left112    exact ⟨none, class⟩113114theorem partitionStep.refined (V leftEnd rightEnd T P : Set, k : Nat)115  requires partition : Partition(V, P)116  requires ends :117    ∀ e ∈ T(leastNatural(disconnectedColour(leftEnd, rightEnd, T, P, k))),118      leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V119  requires some : disconnectedColour(leftEnd, rightEnd, T, P, k) ≠ ∅120  shows partitionStep(V, leftEnd, rightEnd, T, P, k) =121    refineBy(leftEnd, rightEnd,122      T(leastNatural(disconnectedColour(leftEnd, rightEnd, T, P, k))), P)123proof124  have refined := refineBy.partition with partition, ends125  ext X126  constructor127  . intro member128    obtain ⟨_, fixed | refinedX⟩ := member129    . exfalso130      exact some with fixed.left131    . exact refinedX.right132  . intro class133    have subset := (refined.left with X, class).left134    refine ⟨(powerset.membership_iff.backward with subset), _⟩135    right136    exact ⟨some, class⟩137138theorem partitionStep.partition (V E leftEnd rightEnd T P : Set, k : Nat)139  requires graph : Graph(V, E, leftEnd, rightEnd)140  requires decomposition : Decomposition(E, T, k)141  requires partition : Partition(V, P)142  shows Partition(V, partitionStep(V, leftEnd, rightEnd, T, P, k))143proof144  by_cases none : disconnectedColour(leftEnd, rightEnd, T, P, k) = ∅145  . rw partitionStep.fixed with partition, none146    exact partition147  . obtain ⟨colour, _⟩ := disconnectedColour.least with none148    have ends := Decomposition.ends with graph, decomposition, colour149    rw partitionStep.refined with partition, ends, none150    exact refineBy.partition with partition, ends151152-- A fixed step has no disconnected colour: refining along one would change153-- the partition, since that colour is not internally connected.154theorem partitionStep.fixed_colours (V E leftEnd rightEnd T P : Set, k : Nat)155  requires graph : Graph(V, E, leftEnd, rightEnd)156  requires decomposition : Decomposition(E, T, k)157  requires partition : Partition(V, P)158  requires fixed : partitionStep(V, leftEnd, rightEnd, T, P, k) = P159  shows ∀ i ∈ k, InternallyConnected(leftEnd, rightEnd, T(i), P)160proof161  apply disconnectedColour.empty_iff.forward162  by_contra some163  obtain ⟨colour, disconnected⟩ := disconnectedColour.least with some164  have ends := Decomposition.ends with graph, decomposition, colour165  rw partitionStep.refined with partition, ends, some at fixed166  have internal := (refineBy.fixed_iff with partition, ends).forward with fixed167  exact disconnected with internal168169theorem partitionSequence.zero (V leftEnd rightEnd T : Set, k : Nat)170  shows partitionSequence(V, leftEnd, rightEnd, T, k, 0) = {V}171proof172  simp [partitionSequence]173174theorem partitionSequence.succ (V leftEnd rightEnd T : Set, k n : Nat)175  shows partitionSequence(V, leftEnd, rightEnd, T, k, succ(n)) =176    partitionStep(V, leftEnd, rightEnd, T,177      partitionSequence(V, leftEnd, rightEnd, T, k, n), k)178proof179  simp [partitionSequence]180181theorem partitionSequence.partition (V E leftEnd rightEnd T : Set, k n : Nat)182  requires graph : Graph(V, E, leftEnd, rightEnd)183  requires nonempty : V ≠ ∅184  requires decomposition : Decomposition(E, T, k)185  shows Partition(V, partitionSequence(V, leftEnd, rightEnd, T, k, n))186proof187  induction n188  | zero =>189    rw partitionSequence.zero190    constructor191    . intros X member192      rw (singleton.membership.forward with member)193      exact ⟨Subset.reflexive, nonempty⟩194    constructor195    . intros X memberX Y memberY different196      have sameX := singleton.membership.forward with memberX197      have sameY := singleton.membership.forward with memberY198      exfalso199      cc200    . intros v inV201      exact ⟨V, singleton.self, inV⟩202  | succ(m) using ih =>203    rw partitionSequence.succ204    exact partitionStep.partition with graph, decomposition, ih205206theorem partitionSequence.refines (V E leftEnd rightEnd T : Set, k n : Nat)207  requires graph : Graph(V, E, leftEnd, rightEnd)208  requires decomposition : Decomposition(E, T, k)209  shows Refines(partitionSequence(V, leftEnd, rightEnd, T, k, succ(n)),210    partitionSequence(V, leftEnd, rightEnd, T, k, n))211proof212  rw partitionSequence.succ213  intros X member214  obtain ⟨_, fixed | refined⟩ := member215  . exact ⟨X, fixed.right, Subset.reflexive⟩216  . have refines : Refines(refineBy(leftEnd, rightEnd,217        T(leastNatural(disconnectedColour(leftEnd, rightEnd, T,218          partitionSequence(V, leftEnd, rightEnd, T, k, n), k))),219        partitionSequence(V, leftEnd, rightEnd, T, k, n)),220      partitionSequence(V, leftEnd, rightEnd, T, k, n)) := refineBy.refines221    exact refines with X, refined.right222223-- Two classes of a partition sharing a vertex are one class.224theorem Partition.eq_of_member (V P X Y v : Set)225  requires partition : Partition(V, P)226  requires classX : X ∈ P227  requires classY : Y ∈ P228  requires inX : v ∈ X229  requires inY : v ∈ Y230  shows X = Y231proof232  by_contra different233  exact partition.right.left with X, classX, Y, classY, different, v, inX, inY234235-- The class map v ↦ classOf(P, v) sends V onto the classes of P, so a236-- partition of a finite set has at most |V| classes.237defgraph classMap (V P : Set) (v ∈ V) : 𝒫(⋃(P)) := classOf(P, v)238proof239  apply powerset.membership_iff.backward240  have classes : classesContaining(P, v) ⊆ P241    intros X class242    exact class.left243  unfold classOf244  exact union.monotone with classes245246theorem classMap.image (V P : Set)247  requires partition : Partition(V, P)248  shows functionImage(classMap(V, P), V, 𝒫(⋃(P))) = P249proof250  ext X251  constructor252  . intro inImage253    obtain ⟨_, v, inV, rfl⟩ := inImage254    rw classMap.value with inV255    exact (classOf.member with partition, inV).left256  . intro class257    obtain ⟨v, inX⟩ :=258      Nonempty.of_ne_empty with (partition.left with X, class).right259    have inV := (partition.left with X, class).left with v, inX260    have value := classMap.value at V, P, v with inV261    rw (classOf.eq_of_member with partition.right.left, class, inX) at value262    have inPowerset : X ∈ 𝒫(⋃(P)) :=263      powerset.membership_iff.backward with (union.subset_of_member with class)264    symm at value265    exact ⟨inPowerset, v, inV, value⟩266267theorem Partition.cardinality_le (V P : Set)268  requires finiteVertices : Finite(V)269  requires partition : Partition(V, P)270  shows cardinality(P) ≤ cardinality(V)271proof272  have bound := cardinality.image_le with273    (classMap.function at V, P), Subset.reflexive, finiteVertices274  rwa classMap.image with partition at bound275276-- The coarse class of a class Y of a refinement: the class of P holding Y.277def coarseClasses (P Y : Set) : Set := { X ∈ P | Y ⊆ X }278279def coarseClass (P Y : Set) : Set := ⋃(coarseClasses(P, Y))280281theorem coarseClass.membership (P Y z : Set)282  shows z ∈ coarseClass(P, Y) ↔ ∃ X ∈ P, Y ⊆ X ∧ z ∈ X283proof284  simp [coarseClass, coarseClasses, union.membership]285286theorem coarseClass.eq_of_subset (V P X Y : Set)287  requires partition : Partition(V, P)288  requires class : X ∈ P289  requires subset : Y ⊆ X290  requires nonempty : Y ≠ ∅291  shows coarseClass(P, Y) = X292proof293  obtain ⟨v, inY⟩ := Nonempty.of_ne_empty with nonempty294  ext z295  rw coarseClass.membership296  constructor297  . intro inUnion298    obtain ⟨W, classW, subsetW, inW⟩ := inUnion299    have same := Partition.eq_of_member with300      partition, classW, class, (subsetW with v, inY), (subset with v, inY)301    rw same at inW302    exact inW303  . intro inX304    exact ⟨X, class, subset, inX⟩305306defgraph coarseMap (P Q : Set) (Y ∈ Q) : 𝒫(⋃(P)) := coarseClass(P, Y)307proof308  apply powerset.membership_iff.backward309  have classes : coarseClasses(P, Y) ⊆ P310    intros X class311    exact class.left312  unfold coarseClass313  exact union.monotone with classes314315theorem coarseMap.value_of_subset (V P Q X Y : Set)316  requires partition : Partition(V, P)317  requires finer : Partition(V, Q)318  requires classX : X ∈ P319  requires classY : Y ∈ Q320  requires subset : Y ⊆ X321  shows coarseMap(P, Q)(Y) = X322proof323  rw coarseMap.value with classY324  exact coarseClass.eq_of_subset with325    partition, classX, subset, (finer.left with Y, classY).right326327theorem Refines.transitive (P Q R : Set)328  requires first : Refines(P, Q)329  requires second : Refines(Q, R)330  shows Refines(P, R)331proof332  intros X class333  obtain ⟨Y, classY, subsetY⟩ := first with X, class334  obtain ⟨Z, classZ, subsetZ⟩ := second with Y, classY335  exact ⟨Z, classZ, (Subset.transitive with subsetY, subsetZ)⟩336337-- A proper refinement puts two classes of Q inside one class of P: were338-- every class of P to hold at most one class of Q, that class would fill339-- it, and Q would be P.340theorem Refines.two_classes (V P Q : Set)341  requires partition : Partition(V, P)342  requires finer : Partition(V, Q)343  requires refines : Refines(Q, P)344  requires different : Q ≠ P345  shows ∃ X ∈ P, ∃ Y ∈ Q, ∃ Z ∈ Q, Y ≠ Z ∧ Y ⊆ X ∧ Z ⊆ X346proof347  by_contra none348  have fills : ∀ X ∈ P, ∀ Y ∈ Q, Y ⊆ X → Y = X349    intros X classX Y classY subset350    apply Subset.antisymmetric with subset351    intros w inX352    have inV := (partition.left with X, classX).left with w, inX353    obtain ⟨Z, classZ, inZ⟩ := finer.right.right with w, inV354    obtain ⟨W, classW, subsetZ⟩ := refines with Z, classZ355    have sameX := Partition.eq_of_member with356      partition, classW, classX, (subsetZ with w, inZ), inX357    rw sameX at subsetZ358    have sameY : Y = Z359      by_contra distinct360      exact none with361        ⟨X, classX, Y, classY, Z, classZ, distinct, subset, subsetZ⟩362    rw sameY363    exact inZ364  apply different365  ext X366  constructor367  . intro classX368    obtain ⟨Y, classY, subset⟩ := refines with X, classX369    rw (fills with Y, classY, X, classX, subset)370    exact classY371  . intro classX372    obtain ⟨v, inX⟩ :=373      Nonempty.of_ne_empty with (partition.left with X, classX).right374    have inV := (partition.left with X, classX).left with v, inX375    obtain ⟨Y, classY, inY⟩ := finer.right.right with v, inV376    obtain ⟨W, classW, subsetY⟩ := refines with Y, classY377    have sameX := Partition.eq_of_member with378      partition, classW, classX, (subsetY with v, inY), inX379    rw sameX at subsetY380    rw ← (fills with X, classX, Y, classY, subsetY)381    exact classY382383-- A proper refinement of a partition of a finite set has strictly more384-- classes: the coarse-class map from Q onto P identifies two classes, so385-- P is already the image of Q less one class.386theorem Refines.cardinality_lt (V P Q : Set)387  requires finiteVertices : Finite(V)388  requires partition : Partition(V, P)389  requires finer : Partition(V, Q)390  requires refines : Refines(Q, P)391  requires different : Q ≠ P392  shows cardinality(P) < cardinality(Q)393proof394  obtain ⟨X, classX, Y, classY, Z, classZ, distinct, subsetY, subsetZ⟩ :=395    Refines.two_classes with partition, finer, refines, different396  have finiteP := Partition.finite with finiteVertices, partition397  have finiteQ := Partition.finite with finiteVertices, finer398  have rest := difference.subset_left at Q, {Y}399  have finiteRest := Finite.subset with finiteQ, rest400  have function := coarseMap.function at P, Q401  have covered : P ⊆ functionImage(coarseMap(P, Q), Q ∖ {Y}, 𝒫(⋃(P)))402    intros W classW403    obtain ⟨v, inW⟩ :=404      Nonempty.of_ne_empty with (partition.left with W, classW).right405    have inV := (partition.left with W, classW).left with v, inW406    obtain ⟨U, classU, inU⟩ := finer.right.right with v, inV407    have inPowerset : W ∈ 𝒫(⋃(P)) :=408      powerset.membership_iff.backward with (union.subset_of_member with classW)409    by_cases same : U = Y410    . -- v lies in Y ⊆ X, so W is X, the coarse class of Z as well.411      rw same at inU412      have sameW := Partition.eq_of_member with413        partition, classW, classX, inW, (subsetY with v, inU)414      have inRest : Z ∈ Q ∖ {Y} by simp [classZ, distinct]415      have value := coarseMap.value_of_subset with416        partition, finer, classX, classZ, subsetZ417      refine ⟨inPowerset, Z, inRest, _⟩418      rw [value, sameW]419    . have inRest : U ∈ Q ∖ {Y} by simp [classU, same]420      obtain ⟨R, classR, subsetU⟩ := refines with U, classU421      have sameW := Partition.eq_of_member with422        partition, classW, classR, inW, (subsetU with v, inU)423      have value := coarseMap.value_of_subset with424        partition, finer, classR, classU, subsetU425      refine ⟨inPowerset, U, inRest, _⟩426      rw [value, sameW]427  have finiteImage := Finite.function_image with function, finiteRest, rest428  have lower := cardinality.monotone with finiteImage, covered429  have upper := cardinality.image_le with function, rest, finiteRest430  have removed := cardinality.remove_add_one with finiteQ, classY431  arith432433-- While the sequence keeps moving it gains a class at every step.434theorem partitionSequence.grows (V E leftEnd rightEnd T : Set, k n : Nat)435  requires graph : Graph(V, E, leftEnd, rightEnd)436  requires finiteVertices : Finite(V)437  requires nonempty : V ≠ ∅438  requires decomposition : Decomposition(E, T, k)439  requires moving : ∀ i ∈ n,440    partitionSequence(V, leftEnd, rightEnd, T, k, succ(i)) ≠441      partitionSequence(V, leftEnd, rightEnd, T, k, i)442  shows n + 1 ≤ cardinality(partitionSequence(V, leftEnd, rightEnd, T, k, n))443proof444  induction n445  | zero =>446    intro moving447    rw [partitionSequence.zero, cardinality.singleton]448    arith449  | succ(m) using ih =>450    intro moving451    have earlier : ∀ i ∈ m,452        partitionSequence(V, leftEnd, rightEnd, T, k, succ(i)) ≠453          partitionSequence(V, leftEnd, rightEnd, T, k, i)454      intros i member455      have inSucc : i ∈ succ(m) by simp [member]456      exact moving with i, inSucc457    have bound := ih with earlier458    have self : m ∈ succ(m) by simp459    have step := moving with m, self460    have coarse :461        Partition(V, partitionSequence(V, leftEnd, rightEnd, T, k, m)) :=462      partitionSequence.partition with graph, nonempty, decomposition463    have fine :464        Partition(V, partitionSequence(V, leftEnd, rightEnd, T, k, succ(m))) :=465      partitionSequence.partition with graph, nonempty, decomposition466    have refines := partitionSequence.refines467      at V, E, leftEnd, rightEnd, T, k, m with graph, decomposition468    have less := Refines.cardinality_lt with469      finiteVertices, coarse, fine, refines, step470    arith471472-- A strictly refining chain of partitions of a finite set has at most |V|473-- steps, so the sequence is fixed from some stage on.474theorem partitionSequence.stabilises (V E leftEnd rightEnd T : Set, k : Nat)475  requires graph : Graph(V, E, leftEnd, rightEnd)476  requires finiteVertices : Finite(V)477  requires nonempty : V ≠ ∅478  requires decomposition : Decomposition(E, T, k)479  shows ∃ n ∈ ℕ, n ≤ cardinality(V) ∧480    partitionSequence(V, leftEnd, rightEnd, T, k, succ(n)) =481      partitionSequence(V, leftEnd, rightEnd, T, k, n)482proof483  by_contra none484  have natV := cardinality.nat with finiteVertices485  -- Were no stage up to |V| fixed, stage |V| + 1 would have |V| + 2 classes.486  have moving : ∀ i ∈ succ(cardinality(V)),487      partitionSequence(V, leftEnd, rightEnd, T, k, succ(i)) ≠488        partitionSequence(V, leftEnd, rightEnd, T, k, i)489    intros i member490    have natural := natural.member at succ(cardinality(V)) with i, member491    have less := Less.of_membership at i, succ(cardinality(V)) with member492    have below : i ≤ cardinality(V) by arith493    intro fixed494    exact none with ⟨i, (nat.omega.forward with natural), below, fixed⟩495  have grown := partitionSequence.grows with496    graph, finiteVertices, nonempty, decomposition, moving497  have stage : Partition(V,498      partitionSequence(V, leftEnd, rightEnd, T, k, succ(cardinality(V)))) :=499    partitionSequence.partition with graph, nonempty, decomposition500  have bound := Partition.cardinality_le with finiteVertices, stage501  arith502503-- Once fixed, the sequence stays fixed.504theorem partitionSequence.fixed_from (V leftEnd rightEnd T : Set, k n d : Nat)505  requires fixed : partitionSequence(V, leftEnd, rightEnd, T, k, succ(n)) =506    partitionSequence(V, leftEnd, rightEnd, T, k, n)507  shows partitionSequence(V, leftEnd, rightEnd, T, k, n + d) =508    partitionSequence(V, leftEnd, rightEnd, T, k, n)509proof510  induction d511  | zero =>512    rw add.right_unit513  | succ(m) using ih =>514    rw [add.succ_right, partitionSequence.succ, ih, ← partitionSequence.succ]515    exact fixed516517-- The stable partition P_∞ and, on it, every colour is internally connected.518def stablePartition (V leftEnd rightEnd T : Set, k : Nat) : Set :=519  partitionSequence(V, leftEnd, rightEnd, T, k, cardinality(V))520521theorem stablePartition.internal (V E leftEnd rightEnd T : Set, k : Nat)522  requires graph : Graph(V, E, leftEnd, rightEnd)523  requires finiteVertices : Finite(V)524  requires nonempty : V ≠ ∅525  requires decomposition : Decomposition(E, T, k)526  shows ∀ i ∈ k, InternallyConnected(leftEnd, rightEnd, T(i),527    stablePartition(V, leftEnd, rightEnd, T, k))528proof529  obtain ⟨n, natural, below, fixed⟩ := partitionSequence.stabilises with530    graph, finiteVertices, nonempty, decomposition531  have nNat := nat.omega.backward with natural532  obtain ⟨d, dNat, sum⟩ := below533  have same := partitionSequence.fixed_from at V, leftEnd, rightEnd, T, k, n, d534    with fixed535  rw partitionSequence.succ at fixed536  have internal := partitionStep.fixed_colours with graph, decomposition,537    (partitionSequence.partition with graph, nonempty, decomposition), fixed538  intros i colour539  unfold stablePartition540  rw [← sum, same]541  exact internal with i, colour542