bm : {r} (fin r, r >= 1) => [2*r] -> [2*r] bm B = (B @@ [0,2..2*r-2]) # (B @@ [1,3..2*r-1])