The link-homotopy relation is a congruence for the concatenation product (Lemma 3.4)

import Mathlib
import Definitions.Def_HGL_alg
import Definitions.Def_HGL_tor

namespace HGL

/-!  Milestone 1 (Lemma 3.4): the link-homotopy equivalence relation is
compatible with concatenation: if two generalized string links are
link-homotopic, then so are the products with any other generalized string
link, on either side, and componentwise products of homotopic links are
homotopic. The proof lifts the one-sided compatibility of the elementary
moves through the equivalence closure by induction. -/
theorem homotopy_congruence {n g : ℕ} {B S Cl : Type*} [Group B] [Monoid S] [Group Cl]
    (W : LinkHomotopyWorld n g B S Cl) :
    ∀ s t u v : S, EqvGen W.moves s t → EqvGen W.moves u v →
      EqvGen W.moves (s * u) (t * v) := by sorry

end HGL