全ての証明がLEANを通せる形にすべきだとは思わんが、
通しにくいってことはそれなりに説明を要するってことで自明ではないってことは正しいよな。