既存の公理系から形式的に証明を書き下せればいいんだろ？
できなければ万人が納得できる公理を追加してもいい
本人はこれ以上面倒なことはやらなさそうだから力わざの得意なやつがやればいいのに