永田・可換体論の「自明」を自動証明できるレベルじゃなきゃダメだろw