for a, b being Ordinal holds a (+) (succ b) = succ (a (+) b)