Insertion maps into the splitting-chain stages

The insertion of a single module letter into a two-index splitting-chain stage, in the three parts below: the insertions themselves (Base.lean) and the laws they satisfy against the stage multiplication and the seed transition, in the first slot (FirstSlot.lean) and in the second (SecondSlot.lean).