theorem :: ORDINAL7:78

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