求めすぎかもしれないが多分俺じゃ証明の検証できないから
可能ならCoqでの証明つけてほしい。