否定導入は直接証明
矛盾によらない証明のほうが迂回している