任意排列到2循环的文字证明.lean

1234

比如
  4231 4321
4321 = 操作[14][23]
  2134 3124 4123
4123 = 操作[12][13][14]


任意Sn中的元素：(N_1N_2N_3...N_m)
证明：[1?][1?]....[2?][2?]....[(n-1)?]