for n being Nat holds square-downarrow n = [:(Segm n),(Segm n):]