>>898
2つの命題のステートメントが違うっぽい。
異なる命題を証明してるのなら証明の長さが異なるのは当然。